[Ur] Polymorphic datatype needed too late

Adam Chlipala adamc at csail.mit.edu
Wed Feb 24 14:20:18 EST 2016


On 02/24/2016 02:07 PM, Benjamin Barenblat wrote:
>    datatype tree a =
>        Leaf of a
>      | Node of list (tree a)
>
> [...]
>
>    val nothing : tree (transaction int) = Node []

Sorry, this instantiation of the [tree] type family is going to be a 
no-go!  In server-side code, no first-class functions are allowed to 
remain after compiler optimizations, and a [transaction t] is 
represented like (effectful) [unit -> t] internally.  It would all work 
fine for client-side code, though.

Also, I suggest rewriting the beginning of your [mapM] like this, since 
the compiler gets confused, in polymorphic specialization, when 
non-type-level parameters come before type-level parameters.
     fun mapM
         [m ::: Type -> Type] [a ::: Type] [b ::: Type] (_ : monad m)



More information about the Ur mailing list