[Haskell-cafe] type families and type signatures
Martin Sulzmann
martin.sulzmann at gmail.com
Wed Apr 9 05:57:09 EDT 2008
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
More information about the Haskell-Cafe
mailing list