typechecking too eager?
The following code should compile (If the constructor is valid, so is the function): data Test = Test (forall a . a) test a = Test a However this fails to compile with the following error: Test.hs:9:9: Inferred type is less polymorphic than expected Quantified type variable `a' escapes It is mentioned in the environment: test :: a -> Test (bound at Test.hs:9:0) a :: a (bound at Test.hs:9:5) In the first argument of `Test', namely `a' In the definition of `test': test a = Test a I think this should only generate an error once the value of 'a' is known not to be undefined. Keean.
Hi there,
The following code should compile (If the constructor is valid, so is the function):
data Test = Test (forall a . a) test a = Test a
However this fails to compile with the following error:
The current implementation of rank-n polymorphism (which is documented in the paper "Pratical type inference for arbitrary-rank types") does not "guess" polymorphic types for lambda-abstracted values. In this situation, this means that the variable "a" is assumed to have a monorphic type, which then cannot be passed to "Test" as an argument. Knowledge about polymorphism is passed down/inwards, but not up/outwards. This definition typechecks only if you add a type signature: test :: (forall a . a) -> Test If you want to know the reasons, read the paper. It explains the problems very well. Cheers, Andres
So, does that mean that ideally we would like it to type check, but for implementation reasons it cannot easily be done without a type signature? I can use the type signature no problem. Keean. Andres Loeh wrote:
Hi there,
The following code should compile (If the constructor is valid, so is the function):
data Test = Test (forall a . a) test a = Test a
However this fails to compile with the following error:
The current implementation of rank-n polymorphism (which is documented in the paper "Pratical type inference for arbitrary-rank types") does not "guess" polymorphic types for lambda-abstracted values.
In this situation, this means that the variable "a" is assumed to have a monorphic type, which then cannot be passed to "Test" as an argument.
Knowledge about polymorphism is passed down/inwards, but not up/outwards.
This definition typechecks only if you add a type signature:
test :: (forall a . a) -> Test
If you want to know the reasons, read the paper. It explains the problems very well.
Cheers, Andres
So, does that mean that ideally we would like it to type check, but for implementation reasons it cannot easily be done without a type signature?
Not purely for implementation reasons, but also because of theoretical limitations. Depending on what fragment of System F you want to allow, you lose either decidability of type inference or the principal types property if you do not choose to require explicit type signatures. There are certainly design choices here, and one can certainly implement a system that would infer a type for your example without an explicit signature. However, the current implementation has the advantage of (a) being not difficult to implement, and (b) having clear rules for when explicit type signatures are required (the exact rules are given in the "Practical type inference ..." paper by Peyton Jones and Shields). A more powerful alternative is described in the "MLF" paper by Le Botlan and Remy. The use of type signatures when things get difficult isn't uncommon in Haskell: type signatures are required for functions involving polymorphic recursion, and for functions involving ambiguous overloading, and nowadays for some functions that make use of GADTs. Cheers, Andres
participants (2)
-
Andres Loeh -
Keean Schupke