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:[EMAIL PROTECTED]
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
