[Caml-list] problem to use gadt

[Caml-list] problem to use gadt

[Nicolas Boulay]

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

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: 1301 bytes --]

RE: [Caml-list] problem to use gadt

[David Allsopp]

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?

HTH,


David

Re: [Caml-list] problem to use gadt

[Nicolas Boulay]

[-- 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 --]

Re: [Caml-list] problem to use gadt

[Gabriel Scherer]

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

Re: [Caml-list] problem to use gadt

[Nicolas Boulay]

[-- 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 --]