Hello Manuel, Wednesday, September 6, 2006, 9:17:46 PM, you wrote:
So, both features are truly orthogonal and, in fact, they are synergetic! More precisely, an alternative syntax for Löh/Hinze open types are overlapping type families. So, we might define S alternatively as
data family S :: * data instance S = S1 data instance S = S2
to be exact, it's alternative syntax for GADT "data S = S1 | S2" while open types just allows to split GADT definition into several chunks. It seems that you skipped this point - they also propose to use open technique for GADT-style definitions. as a result, while open data types are truly orthogonal to GADT, together they implement something very close to type families. the only difference between GADT+OT vs TF remains:
GADTS+open types: * Local type-refinement in case alternatives
Data families: * Type constraints due to indexes is propagated globally
can you please explain that this means?
In fact, there is nothing essential preventing us from having indexed families of GADTs
for why? the only difference is that TF define a one-to-one relationship (each type index defines just one data constructor) while GADT define one-to-many relationship (one type index may be mapped to several data constructors). are we really need this difference and especially different syntax for such close things? just for curiosity, i was also interested in ideas of type-level programming and invented my own syntax that is more like yours. but really my syntax just based on the syntax of ordinary functions: type BaseType [a] = BaseType a BaseType (Set a) = BaseType a BaseType (Map a b) = BaseType a BaseType a = a is a recursive definition which may be evaluated with first-fit or best-fit strategy data Expr a = If (Expr Bool) (Expr a) (Expr a) Expr Int = Zero Expr Int = Succ (Expr Int) Expr Bool = TRUE Expr Bool = Not (Expr Bool) is alternative syntax for GADT. we may consider it as multi-value function, and 'data' defines functions that maps types into data constructors while 'type' defines functions that maps types into types. going further, why not allow 'type' to define multi-value functions? and vice versa, why not use 'data' to define one-to-one relation by best-fit or first-fit strategy? going further, why not define type of relation in "function" head? so that we can both use 'data' and 'type' to define one-to-one (non-overlapped) type families or one-to-many (overlapped, GADT-style) ones and even select matching strategy here? for example: data nonOverlapped T TTrue = CTrue T TFalse = CFalse data bestFit Eq a b = CFalse Eq a a = CTrue type firstFit Eq a a = TTrue Eq a b = TFalse -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com