[racket] [typed racket] typing monads

From: Eric Tanter (etanter at dcc.uchile.cl)
Date: Thu Oct 20 14:52:09 EDT 2011

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 ...)))

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
> 




Posted on the users mailing list.