[racket] [typed racket] typing monads

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