type problem...

[Pietro Abate <Pietro.Abate@anu.edu.au>]

Hi all,
I'm trying to type-check the continuation monad defined as follows:

module LM =
    struct
        type 'a m = 'a list
        let return x = [x]
        let mzero = []
        let bind m f = List.flatten (List.map f m)
        let mplus = List.append
        let guard b = if b then return () else mzero
    end
;;

module CM
: sig
    type r
    type 'node k = (('node -> 'node m) -> 'node m)
    and 'node m = (r * 'node k LM.m) LM.m

    val return : 'a -> 'a k
    val bind : 'a k -> ('a -> 'b k) -> 'b k
    val callCC : (('a -> 'b k) -> 'a k) -> 'a k
end
    = struct
    type r
    type 'node k = (('node -> 'node m) -> 'node m)
    and 'node m = (r * 'node k LM.m) LM.m

    let return a = (fun k -> k a)
    let bind m f = (fun k -> m (fun x -> f x k))
    let callCC f k1 = ( f (fun x k2 -> k1 x) k1 )
end

if you compile it with ocamlc -rectypes -i ex.ml  the compile says:

Values do not match:
  val bind : (('a -> 'b) -> 'c) -> ('a -> 'd -> 'b) -> 'd -> 'c
is not included in
  val bind : 'a k -> ('a -> 'b k) -> 'b k

but at first sight, these two types should match ... maybe not ...
or at least they do match if the type k is not cyclic...

I think the solution is in Wadler paper
http://portal.acm.org/citation.cfm?id=143169 in section 3.3, but it is not
entirely clear what I should do here ...  to get the right type...


-- 
++ Blog: http://blog.rsise.anu.edu.au/?q=pietro
++ 
++ "All great truths begin as blasphemies." -George Bernard Shaw
++ Please avoid sending me Word or PowerPoint attachments.
   See http://www.fsf.org/philosophy/no-word-attachments.html