Re: [Caml-list] Late adding of type variable constraints

[Markus Mottl <markus.mottl@gmail.com>]

On Wed, Sep 9, 2015 at 3:28 PM, Mikhail Mandrykin <mandrykin@ispras.ru> wrote:
> Probably the defunctionalization encoding used in the paper on Lightweight
> Higher-Kinded Polymorphism in OCaml
> (https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf) can help in some way. The corresponding library and examples
> are available at https://github.com/ocamllabs/higher.

Thanks a lot for this reference and your code.  Though my problem
still seems slightly different, I found this to be a very interesting
paper.  I remember reading Reynolds' work on defunctionalization many
years ago, and it's fascinating how his work translates from the
object to the type language.

> The implementation used in the library doesn't perfectly fit the case, because
> the suggested encoding puts the type `t' capturing the type skeleton on an
> unknown depth inside the list of type constructor applications.  I tried the
> following slight variation on the initial encoding:

I think the main problem for me is not so much capturing the skeleton,
which the initial approach does just fine, but that type constraints
on the polymorphic variables are maintained with mapper functions.
Maybe the more complicated approaches can be combined to solve the
problem, but that is likely not trivial.

> module Newtype1 (T : sig type 'a t end) =
> struct
>   type 'a s = 'a T.t
>   type t
>   type (_, _) typ += Mk : 'a T.t -> (('a, nil) app, t) typ
>   let inj v = Mk v
>   let prj (Mk v) = v
> end

The compiler will warn above that "prj" is not exhaustive.  If I
understand this correctly, the reasoning is that it's impossible for
two GADT constructors to yield the same type so the warning should be
spurious.  But wouldn't this require making Newtype1 a generative
functor (i.e. adding "()")?  Otherwise the type "t" could be seen as
equivalent if Newtype1 is applied to the same module more than once,
which would allow for more than one "Mk" case and could hence cause a
runtime match error.

I think for the while being I'll just stick to the syntactic approach.
Users who want to extend the number of base types to be mapped over
would have to include code with "Pair", "Option", etc. within an
environment with augmented constraints.

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com