Re: [Haskell-cafe] Type families and polymorphism
Dan Doel wrote: Hope that helps. It does, thanks! Jeremy -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and polymorphism
Jeremy Yallop wrote:
Why does compiling the following program give an error?
{-# LANGUAGE TypeFamilies, RankNTypes #-}
type family TF a
identity :: (forall a. TF a) - (forall a. TF a)
identity x = x
GHC 6.10.3 gives me:
Couldn't match expected type `TF a1' against inferred type `TF a'
In the expression: x
In the definition of `identity': identity x = x
The error message is slightly better in GHC head:
Couldn't match expected type `TF a1' against inferred type `TF a'
NB: `TF' is a type function, and may not be injective
In the expression: x
In the definition of `identity': identity x = x
Dan Doel already explained how the lack of injectivity leads to a type
checking error.
FWIW, the same code would work with a data family, because data families
are injective.
regards,
Bertram
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and polymorphism
On Jul 11, 2009, at 14:31 , Jeremy Yallop wrote:
Why does compiling the following program give an error?
{-# LANGUAGE TypeFamilies, RankNTypes #-}
type family TF a
identity :: (forall a. TF a) - (forall a. TF a)
identity x = x
The scope of each a is the surrounding parentheses, so the de facto
type is TF a - TF b. Or, put otherwise, you're saying that for *any*
type (TF a) you can produce *any* type (TF a) (because of the
delimited forall-s), but then the code asserts that they are the same
type.
--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com
system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu
electrical and computer engineering, carnegie mellon universityKF8NH
PGP.sig
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and polymorphism
* Brandon S. Allbery KF8NH allb...@ece.cmu.edu [2009-07-11 17:01:35-0400]
On Jul 11, 2009, at 14:31 , Jeremy Yallop wrote:
Why does compiling the following program give an error?
{-# LANGUAGE TypeFamilies, RankNTypes #-}
type family TF a
identity :: (forall a. TF a) - (forall a. TF a)
identity x = x
The scope of each a is the surrounding parentheses, so the de facto type
is TF a - TF b. Or, put otherwise, you're saying that for *any* type (TF
a)
No, for any (forall a. TF a), which should make the difference.
you can produce *any* type (TF a) (because of the delimited forall-s),
but then the code asserts that they are the same type.
--
Roman I. Cheplyaka :: http://ro-che.info/
Don't let school get in the way of your education. - Mark Twain
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and polymorphism
On Saturday 11 July 2009 2:31:28 pm Jeremy Yallop wrote:
Why does compiling the following program give an error?
{-# LANGUAGE TypeFamilies, RankNTypes #-}
type family TF a
identity :: (forall a. TF a) - (forall a. TF a)
identity x = x
GHC 6.10.3 gives me:
Couldn't match expected type `TF a1' against inferred type `TF a'
In the expression: x
In the definition of `identity': identity x = x
It has to do with the way that type families are checked, and the fact that
they aren't guaranteed to be injective. You can massage the type to look like:
identity :: forall b. (forall a. TF a) - TF b
Which means that the caller gives us a 'b' and a 'forall a. TF a', and wants
us to return a 'TF b'. That sounds fine, but when GHC goes to check things,
things go awry. It instantiates things something like...
x :: TF c (for some fresh c)
TF c ~ TF b (this constraint must be solved for the return type to work)
However, since type families aren't necessarily injective, it can't deduce
c ~ b
since there might well be distinct 'b' and 'c' such that 'TF b ~ TF c'. So, it
fails to come to the conclusion that:
x :: TF b
which is what is actually needed for the function as a whole to type. Thus,
checking fails. I think that's a reasonably accurate description of the
process; if not someone will probably correct me.
One could imagine extensions to solve this. For instance, if you could
(optionally) do something like:
ident...@b x = x...@b
to specifically apply the type variables, the compiler might have an easier
time accepting such things. You can fake it now by having non-family types fix
the variable:
data Witness a -- = W -- if you don't like empty types
identity :: (forall a. Witness a - TF a) - (forall a. Witness a - TF a)
identity x w = x w
This will be accepted, because inference/checking for Witness provides enough
information to deduce the 'c ~ b' above. But of course, it's somewhat less
than ideal.
Hope that helps.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
