haskell-cafe@haskell.org
[Top] [All Lists]

Re: [Haskell-cafe] type families and type signatures

Subject: Re: [Haskell-cafe] type families and type signatures
From: Martin Sulzmann
Date: Wed, 09 Apr 2008 11:57:09 +0200
Claus Reinke wrote:
type family Id a

type instance Id Int = Int

foo :: Id a -> Id a
foo = id n

foo' :: Id a -> Id a
foo' = foo

type function notation is slightly misleading, as it presents
qualified polymorphic types in a form usually reserved for unqualified polymorphic types.

rewriting foo's type helped me to see the ambiguity that
others have pointed out:

foo :: r ~ Id a => r -> r

there's nowhere to get the 'a' from. so unless 'Id' itself is
fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't
really be used. for each type variable, there needs to be
at least one position where it is not used as a type family
parameter.

Correct because type family constructors are injective only.

[Side note: With FDs you can enforce bijection

class Inj a b | a -> b
class Bij a b | a -> b, b -> a
]

it might be useful to issue an ambiguity warning for such types?

perhaps, with closed type families, one might be able to
reason backwards (is there a unique 'a' such that 'Id a ~ Int'?),
as with bidirectional FDs. but if you want to flatten all
'Maybe'-nests, even that direction isn't unique.

True, type checking with closed type families will rely on some form of
solving and then we're more likely to guess (the right) types.

The type checking problem for foo' boils down to verifying the formula

forall a. exists b. Id a ~ Id b

naively, i'd have expected to run into this instead/first:

(forall a. Id a -> Id a) ~ (forall b. Id b -> Id b)

which ought to be true modulo alpha conversion, without guesses,
making 'foo'' as valid/useless as 'foo' itself.

where am i going wrong?

You're notion of subsumption is too strong here.
I've been using


 (forall as. C => t) <= (forall bs. C' => t')

iff

 forall bs. (C'  implies exist bs. (C /\ t=t'))

where

(forall as. C => t) is the inferred type

(forall bs. C' => t') is the annotated type

Makes sense?


Even if we establish

(forall a. Id a -> Id a) ~ (forall b. Id b -> Id b)

we'd need to guess a ~ b
(which is of course obvious)

claus

ps. i find these examples and discussions helpful, if often initially
       puzzling - they help to clear up weak spots in the practice
of type family use, understanding, and implementation, thereby improving all while making families more familiar!-)
Absolutely!

Martin


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/haskell-cafe

<Prev in Thread] Current Thread [Next in Thread>