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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
