Why does the code below not pass the type checker? If I could explictly parameterize y with the type constructor Id (as e.g. in System F), then 'y Id' should have the type Int -> Int and hence "y Id x" should be OK, but with Haskell's implicit type parameters it does not work. So, how can I make this work? Klaus ------------ type Id a = a x :: Id Int x = undefined y :: (a Int) -> (a Int) y = undefined test = y x Error: Couldn't match expected type `a Int' against inferred type `Id Int' In the first argument of `y', namely `x' In the expression: y x In the definition of `test': test = y x -- View this message in context: http://www.nabble.com/Question-about-kinds-tp17701553p17701553.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
On Fri, 2008-06-06 at 15:41 -0700, Klaus Ostermann wrote:
Why does the code below not pass the type checker?
If I could explictly parameterize y with the type constructor Id (as e.g. in System F), then 'y Id' should have the type Int -> Int and hence "y Id x" should be OK, but with Haskell's implicit type parameters it does not work.
So, how can I make this work?
Klaus ------------
type Id a = a
x :: Id Int x = undefined
y :: (a Int) -> (a Int) y = undefined
test = y x
Error: Couldn't match expected type `a Int' against inferred type `Id Int' In the first argument of `y', namely `x' In the expression: y x In the definition of `test': test = y x
Down this path is higher-order unification which is undecidable. You can use a newtype.
On Fri, Jun 6, 2008 at 4:41 PM, Klaus Ostermann
type Id a = a
x :: Id Int x = undefined
y :: (a Int) -> (a Int) y = undefined
In "a Int", "a" refers to any type constructor, not any type function. So the best you can do is: newtype Id a = Id a -- rest as before Luke
On Fri, Jun 06, 2008 at 03:41:07PM -0700, Klaus Ostermann wrote:
Why does the code below not pass the type checker?
If I could explictly parameterize y with the type constructor Id (as e.g. in System F), then 'y Id' should have the type Int -> Int and hence "y Id x" should be OK, but with Haskell's implicit type parameters it does not work.
The type of 'Id' is expanded to simply 'Int', and 'Int' does not unify with 'm a' for any type constructor 'm': Haskell's type level functions are always unevaluated (type synonyms don't count: they are always expanded). So, if you wanted to to this, you'd need to do newtype Id a = Id a Of course, now your values need to be tagged as well. Edsko
"type" declarations are not first-class; treat them more like macro
expansions. In particular, you cannot make a function polymorphic
over a type declaration.
You can make this typecheck using a "data" or "newtype" declaration for Id:
newtype Id x = Identity x
(or)
data Id x = Identity x
You do need to wrap/unwrap the "Identity" constructor then.
-- ryan
On Fri, Jun 6, 2008 at 3:41 PM, Klaus Ostermann
Why does the code below not pass the type checker?
If I could explictly parameterize y with the type constructor Id (as e.g. in System F), then 'y Id' should have the type Int -> Int and hence "y Id x" should be OK, but with Haskell's implicit type parameters it does not work.
So, how can I make this work?
Klaus ------------
type Id a = a
x :: Id Int x = undefined
y :: (a Int) -> (a Int) y = undefined
test = y x
Error: Couldn't match expected type `a Int' against inferred type `Id Int' In the first argument of `y', namely `x' In the expression: y x In the definition of `test': test = y x
short answer: use newtype instead of type (and check the language spec for the difference between the two).
Why does the code below not pass the type checker?
because of the type error?-) seriously, though, it is useful to accompany such questions with some indication of what you're trying to do, to put a cap on the wide variety of possible answers (depending on what it is you're trying to achieve, there are many different techniques or tricks that might apply), and to have something to compare the non-working code against (also in case the intention needs to be edited before working code can be suggested).
If I could explictly parameterize y with the type constructor Id (as e.g. in System F), then 'y Id' should have the type Int -> Int and hence "y Id x" should be OK, but with Haskell's implicit type parameters it does not work.
schemes that rely on implicit 'Id' tend to be doomed to failure in haskell and often suggest a need to get better acquainted with the limitations of haskell's type system (such schemes often arise from invalid generalisations of promising features, and many of us, myself included, have fallen into that trap at one point or other, often while working with type constructor classes): - type synonyms are syntactic macros, not part of the type system proper; the error message is a bit confusing by trying to be helpful (giving type synonym applications instead of their expansion: the type system has seen 'Int', not 'Id Int') - things of kind (* -> *) are type _constructors_, not arbitrary type functions - type families are a restricted kind of type function, but can only be applied forwards (F t1 ~> t2), not be inferred or abstracted over simplified, if the type system had to _infer_ 'Id' (or the composition of type constructors, a related favourite;-), it could do so anywhere, any number of times. in haskell's approach to this, programmers have to indicate where such things are meant to occur (eg, by using newtypes). hth, claus
So, how can I make this work?
Klaus ------------
type Id a = a
x :: Id Int x = undefined
y :: (a Int) -> (a Int) y = undefined
test = y x
Error: Couldn't match expected type `a Int' against inferred type `Id Int' In the first argument of `y', namely `x' In the expression: y x In the definition of `test': test = y x
-- View this message in context: http://www.nabble.com/Question-about-kinds-tp17701553p17701553.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (6)
-
Claus Reinke -
Derek Elkins -
Edsko de Vries -
Klaus Ostermann -
Luke Palmer -
Ryan Ingram