23 Aug 2012 13:27
Rigid skolem type variable escaping scope
<oleg <at> okmij.org>
2012-08-23 11:27:02 GMT
2012-08-23 11:27:02 GMT
Matthew Steele asked why foo type-checks and bar doesn't:
> class FooClass a where ...
>
> foo :: (forall a. (FooClass a) => a -> Int) -> Bool
> foo fn = ...
>
> newtype IntFn a = IntFn (a -> Int)
>
> bar :: (forall a. (FooClass a) => IntFn a) -> Bool
> bar (IntFn fn) = foo fn
This and further questions become much simpler if we get a bit more
explicit. Imagine we cannot write type signatures like those of foo
and bar (no higher-ranked type signatures). But we can define
higher-rank newtypes. Since we can't give foo the higher-rank
signature, we must re-write it, introducing the auxiliary
newtype FaI.
> {-# LANGUAGE Rank2Types #-}
> class FooClass a where m :: a
>
> instance FooClass Int where m = 10
>
> newtype FaI = FaI{unFaI :: forall a. (FooClass a) => a -> Int}
> foo :: FaI -> Bool
> foo fn = ((unFaI fn)::(Char->Int)) m > 0
(Continue reading)
RSS Feed