[racket] [typed racket] typing monads

On Thu, Oct 20, 2011 at 12:52 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> Thanks Sam,
>
> Actually, that's not what we're after.
>
> In untyped Racket, we have a struct monad:
>
> (struct monad
>  (;; A -> M A
>   return
>   ;; A -> (A -> M B) -> M B
>   bind))
>
> Then we have several instantiations (exception, state, what-have-you):
> (define my-fancy-monad (monad (lambda ...) (lambda ...)))

How do you protect against combing the Maybe monad's bind with the
State monad's bind? Monads are more like objects where the methods
have to take the same kind of thing, not just some higher level monad
class.

Jay

>
> It is feasible to type the particular instantiations (the return/bind functions we need in each case), but we'd like to type the monad struct itself.
> The question is what to do about M?
>
> For now we're falling back on Any:
>
> (struct: monad ([return : Any]
>                [bind : Any]))
>
> Can we do better?
>
> I hope that's a bit clearer.
>
> Thanks,
>
> -- Éric
>
> On Oct 20, 2011, at 2:51 PM, Sam Tobin-Hochstadt wrote:
>
>> On Thu, Oct 20, 2011 at 10:45 AM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
>>> Hi,
>>>
>>> Is there a way to type a monad?
>>>
>>> For example in OCaml:
>>>
>>> module type MonadRequirements = sig
>>>    type ‘a t
>>>    val bind : ‘a t -> (‘a -> ‘b t) -> ‘b t
>>>    val return : ‘a -> ‘a t
>>> end;;
>>>
>>> In Typed Racket we can use a polymorphic struct to have the parametrization by 'a and 'b, but is it possible to specify the abstract type constructor t?
>>
>> Types for monads will work just fine in Typed Racket.  However, Typed
>> Racket doesn't provide type abstraction over and above what plain
>> Racket provides.  You can use structs to ensure that instances of your
>> monad aren't constructed except by `return' and `bind', just like you
>> would in untyped Racket.
>>
>> Also, Racket doesn't have a notion of module interfaces, so there
>> isn't a direct analog of how using 'module type' in OCaml works.
>>
>> Here's a module providing the identity monad in Typed Racket, with
>> structures hiding the contents:
>>
>> #lang typed/racket
>> (struct: (T) wrap ([v : T]))
>> (define-type M wrap)
>> (: return (All (T) T -> (M T)))
>> (define (return x) (wrap x))
>> (: bind (All (T U) (M T) (T -> (M U))-> (M U)))
>> (define (bind x f) (f (wrap-v x)))
>> (provide M return bind)
>>
>> --
>> sam th
>> samth at ccs.neu.edu
>>
>
>
> _________________________________________________
>  For list-related administrative tasks:
>  http://lists.racket-lang.org/listinfo/users
>



-- 
Jay McCarthy <jay at cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93