[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