Re: [Caml-list] problem to use gadt

[Nicolas Boulay <nicolas@boulay.name>]

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

It will not work with a "And".

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

2015-02-15 15:47 GMT+01:00 Gabriel Scherer <gabriel.scherer@gmail.com>:

> The typing rule for Or is rather weird: any type can be used as the
> result type, which is non-standard. You could define a dummy type
> "any"
>
>   type any = Any
>
>   [...]
>
>   | Or : _ t * _ t -> any t
>
> and the output type of Or wouldn't be polymorphic anymore, so the
> value restriction (
> http://caml.inria.fr/resources/doc/faq/core.en.html#weak-type-variables
> ) wouldn't be a problem anymore.
>
> On Sun, Feb 15, 2015 at 2:35 PM, Nicolas Boulay <nicolas@boulay.name>
> 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
> >  | Int : int t
> >  | Float : float t
> >
> > let a = Or (Int, Float)  (*is ok*)
> >
> > let (||)  a b = Or (a, b)
> >
> > let aa = Int || Float (*Error: '_a t, contains type variable that cannot
> be
> > generalized*)
> >
> > 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 ?
> >
> > Nicolas Boulay
>

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