Exceptions

[Bulat Ziganshin]

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 at gmail.com