Re: [Caml-list] problem to use gadt

[Nicolas Boulay <nicolas@boulay.name>]

[-- Attachment #1: Type: text/plain, Size: 1711 bytes --]

2015-02-15 15:44 GMT+01:00 David Allsopp <dra-news@metastack.com>:

> Nicolas Boulay wrote:
> > I try to define my own type system using gadt.
> > But it seems that is complex to mix both type system : mine and the
> ocaml one.
> >
> > This tiny example did not compile:
> > type _ t =
> >  | Or: _ t * _ t -> _ t
>
> Is this definitely what you mean - the "_" is not itself a distinct type
> variable so all three underscores in this instance are different types. cf
> the signature of the constructor:
>
> Or : 'b t * 'c -> 'a t
>
> >  | Int : int t
> >  | Float : float t
> >
> > let a = Or (Int, Float)  (*is ok*)
>
> But again, does it have the type you mean, in this case 'a t?
>
> > let (||)  a b = Or (a, b)
> > let aa = Int || Float (*Error: '_a t, contains type variable that cannot
> be generalized*)
>
> This is a consequence of the value restriction, I think.
>
> > Using an operator make a difference. But how to exprime "don't care"
> > if a choice between 2 types is not possible to be define.  It could
> > be nice if "('a | 'b) t" worked :) Should i use normal sum type, and
> > make all type check by a function ?
>
> So you're saying that you don't care what the type of the two halves of an
> Or is? I don't see the problem you're trying to solve, but I wonder if your
> issue is that you need to pick a concrete type representation for the Or
> constructor. For example, does
>
> Or : _ t * _t -> unit t
>
> solve your problem?
>
>
Not really.

"t" is only a part of my complete type. It also have an "And"

| And : 'a t * 'a t -> 'a t

This "and" works well for "Float or Int" but not for "Or".

let aa = And ((Int || Float), Int) (*won't compile, int t != any t*)


> HTH,
>
>
> David
>

[-- Attachment #2: Type: text/html, Size: 2648 bytes --]