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