Re: Question aboutthe use of an inner forall
At 2002-08-18 18:19, Scott J. wrote:
A question: s is not a type variable as a isn't it?
Both are quantified type variables. But only one of those quantifiers can be placed at the top level of the expression. runST :: forall a. ((forall s. ST s a) -> a)
I mean a can be of type Integer while s cannot.
Well yes, you can specialise "forall a" to Integer. So runST can be specialised to this type: runST ::[special] (forall s. ST s Integer) -> Integer ...whereas you cannot specialise "s" in the same way. Think of it in terms of logic, if for all a: f(a), then by simple specialisation f(Integer). -- Ashley Yakeley, Seattle WA
Ok, a and s are type variables. It may be common usage for computer people but for someone with a math background it is difficult to call forall a a type . In logic one expects a statement in the scope of forall a like this
(forall a) statement. The statement may or may not depend on a.
So let's come backe to runST.
runST ::( forall s) (ST s a )-> a
So I insist what is the statement ST s a ?
Scott
----- Original Message -----
From: "Ashley Yakeley"
At 2002-08-18 18:19, Scott J. wrote:
A question: s is not a type variable as a isn't it?
Both are quantified type variables. But only one of those quantifiers can be placed at the top level of the expression.
runST :: forall a. ((forall s. ST s a) -> a)
I mean a can be of type Integer while s cannot.
Well yes, you can specialise "forall a" to Integer. So runST can be specialised to this type:
runST ::[special] (forall s. ST s Integer) -> Integer
...whereas you cannot specialise "s" in the same way. Think of it in terms of logic, if for all a: f(a), then by simple specialisation f(Integer).
-- Ashley Yakeley, Seattle WA
participants (2)
-
Ashley Yakeley -
Scott J.