2015-02-15 15:44 GMT+01:00 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? > > 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 >