Marnix Klooster wrote (to the Haskell Mailing List):
> (1) a `type' declaration introduces a new type + two anonymous
> coercions;
> [...]
> (4) if an expression is of type A when type B is expected, and a
> coercion function is defined of type A -> B, then it is
> automatically inserted (this is _implicit_ coercion);
> I think that (1) and (4) together give an interpretation of type
> synonyms that works the same in practice as the current Haskell view
> that was cited above.
Your system seems more restrictive. For example
type Fruit = Int
type Apples = Fruit
type Bananas = Fruit
noBananas :: Bananas -> Bool
noBananas bananas
= bananas == 0
yesWeHaveNoBananas
= noBananas 0
yesWeHaveNoApples
= noBananas (0 :: Apples)
is a valid Haskell program. In your system yesWeHaveNoBananas
would be rejected, because there is no coercion :: Int
-> Bananas. Maybe you want add the transitive closure of
anonymous coercions.
(5) if there is a anonymous coercion c1 :: A->B and a anonymous
coercion c2 B->C than there is an anonymous coercion
c3 :: A->C.
You can't add (5) for programmer defined coercions on algebraic
types, because this would make it ambiguous. All in all, it gets
pretty wild.
I would like a type system where yesWeHaveNoBananas would be
accepted and yesWeHaveNoApples would be rejected ("Can't unify
Apples with Bananas"). Perhaps you can accomplish this by doing
restricted type synonym expansions during unification. Like Marnix,
I'm no expert in type systems, so I don't know where this would
lead to.
Haskell 1.3 has the newtype feature, example:
newtype Fruit = Int
newtype Apples = Apples Fruit
newtype Bananas = Bananas Fruit
noBananas :: Bananas -> Bool
noBananas (Bananas bananas)
= bananas == 0
yesWeHaveNoBananas
= noBananas (Bananas 0)
yesWeHaveNoApples
= noBananas (Apples 0)
(Hope this is correct, I don't have a Haskell 1.3 compiler handy)
Maybe this is what I want, but I'm not sure if it's always convenient
to write down the constructors everywhere (even if they don't have a
run time overhead).
Cheers,
Ronny Wichers Schreur
