Re: [Haskell-cafe] Rigid skolem type variable escaping scope
On Aug 23, 2012, at 10:32 PM, wren ng thornton wrote: Now, be careful of something here. The reason this fails is because we're compiling Haskell to System Fc, which is a Church-style lambda calculus (i.e., it explicitly incorporates types into the term language). It is this fact of being Church-style which forces us to instantiate ifn before we can do case analysis on it. If, instead, we were compiling Haskell down to a Curry-style lambda calculus (i.e., pure lambda terms, with types as mere external annotations) then everything would work fine. In the Curry-style world we wouldn't need to instantiate ifn at a specific type before doing case analysis, so we don't have the problem of magicking up a type. And, by parametricity, the function fn can't do anything particular based on the type of its argument, so we don't have the problem of instantiating too early[1]. Okay, I think that's what I was looking for, and that makes perfect sense. Thank you! Of course, (strictly) Curry-style lambda calculi are undecidable after rank-2 polymorphism, and the decidability at rank-2 is pretty wonky. Hence the reason for preferring to compile down to a Church-style lambda calculus. There may be some intermediate style which admits your code and also admits the annotations needed for inference/checking, but I don't know that anyone's explored such a thing. Curry-style calculi tend to be understudied since they go undecidable much more quickly. Gotcha. So if I'm understanding correctly, it sounds like the answer to one of my earlier questions is (very) roughly, Yes, the original version of bar would be typesafe at runtime if the typechecker were magically able to allow it, but GHC doesn't allow it because trying to do so would get us into undecidability nastiness and isn't worth it. Which is sort of what I expected, but I couldn't figure out why; now I know. I think now I will go refresh myself on System F (it's been a while) and read up on System Fc (which I wasn't previously aware of). (-: Cheers, -Matt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
System Fc has another name: GHC Core. You can read it by running 'ghc
-ddump-ds' (or, if you want to see the much later results after
optimization, -ddump-simpl):
For example:
NonGADT.hs:
{-# LANGUAGE TypeFamilies, ExistentialQuantification, GADTs #-}
module NonGADT where
data T a = (a ~ ()) = T
f :: T a - a
f T = ()
x :: T ()
x = T
C:\haskellghc -ddump-ds NonGADT.hs
[1 of 1] Compiling NonGADT ( NonGADT.hs, NonGADT.o )
Desugar (after optimization)
Result size = 17
NonGADT.f :: forall a_a9N. NonGADT.T a_a9N - a_a9N
[LclIdX]
NonGADT.f =
\ (@ a_acv) (ds_dcC :: NonGADT.T a_acv) -
case ds_dcC of _ { NonGADT.T rb_dcE -
GHC.Tuple.() `cast` (Sym rb_dcE :: () ~# a_acv)
}
NonGADT.x :: NonGADT.T ()
[LclIdX]
NonGADT.x = NonGADT.$WT @ () (GHC.Types.Eq# @ * @ () @ () @~ ())
The @ is type application; cast is a system Fc feature that that allows
type equality to be witnessed by terms;
Removing the module names and renaming things to be a bit more readable, we
get:
f :: forall a. T a - a
f = \ (@ a) (x :: T a) - case x of { T c - () `cast` (Sym c :: () ~# a) }
-- Here ~# is an unboxed type equality witness; it gets erased during
compilation.
-- We need Sym c because c :: a ~# () and cast wants to go from () to a, so
the
-- compiler uses Sym to swap the order.
x :: T ()
x = T @() (Eq# @* @() @() @~ ())
-- Eq# seems to be the constructor for ~#; I'm not sure what the ()
syntax is.
-- Notice the kind polymorphism; Eq# takes a kind argument as its first
-- argument, then two type arguments of that kind.
-- ryan
On Fri, Aug 24, 2012 at 2:39 AM, Matthew Steele mdste...@alum.mit.eduwrote:
On Aug 23, 2012, at 10:32 PM, wren ng thornton wrote:
Now, be careful of something here. The reason this fails is because
we're compiling Haskell to System Fc, which is a Church-style lambda
calculus (i.e., it explicitly incorporates types into the term language).
It is this fact of being Church-style which forces us to instantiate ifn
before we can do case analysis on it. If, instead, we were compiling
Haskell down to a Curry-style lambda calculus (i.e., pure lambda terms,
with types as mere external annotations) then everything would work fine.
In the Curry-style world we wouldn't need to instantiate ifn at a specific
type before doing case analysis, so we don't have the problem of magicking
up a type. And, by parametricity, the function fn can't do anything
particular based on the type of its argument, so we don't have the problem
of instantiating too early[1].
Okay, I think that's what I was looking for, and that makes perfect sense.
Thank you!
Of course, (strictly) Curry-style lambda calculi are undecidable after
rank-2 polymorphism, and the decidability at rank-2 is pretty wonky. Hence
the reason for preferring to compile down to a Church-style lambda
calculus. There may be some intermediate style which admits your code and
also admits the annotations needed for inference/checking, but I don't know
that anyone's explored such a thing. Curry-style calculi tend to be
understudied since they go undecidable much more quickly.
Gotcha. So if I'm understanding correctly, it sounds like the answer to
one of my earlier questions is (very) roughly, Yes, the original version
of bar would be typesafe at runtime if the typechecker were magically able
to allow it, but GHC doesn't allow it because trying to do so would get us
into undecidability nastiness and isn't worth it. Which is sort of what I
expected, but I couldn't figure out why; now I know.
I think now I will go refresh myself on System F (it's been a while) and
read up on System Fc (which I wasn't previously aware of). (-:
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Rigid skolem type variable escaping scope
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
We cannot apply fn to a value: we must first remove the wrapper FaI
(and instantiate the type using the explicit annotation -- otherwise
the type-checker has no information how to select the FooClass
instance).
Let's try writing bar in this style. The first attempt
newtype IntFn a = IntFn (a - Int)
newtype FaIntFn = FaIntFn{unFaIntFn:: forall a. FooClass a = IntFn a}
bar :: FaIntFn - Bool
bar (IntFn fn) = foo fn
does not work:
Couldn't match expected type `FaIntFn' with actual type `IntFn t0'
In the pattern: IntFn fn
Indeed, the argument of bar has the type FaIntFn rather than IntFn, so
we cannot pattern-match on IntFn. We must first remove the IntFn
wrapper. For example:
bar :: FaIntFn - Bool
bar x = case unFaIntFn x of
IntFn fn - foo fn
That doesn't work for another reason:
Couldn't match expected type `FaI' with actual type `a0 - Int'
In the first argument of `foo', namely `fn'
In the expression: foo fn
foo requires the argument of the type FaI, but fn is of the type
a0-Int. To get the desired FaI, we have to apply the wrapper FaI:
bar :: FaIntFn - Bool
bar x = case unFaIntFn x of
IntFn fn - foo (FaI fn)
And now we get the desired error message, which should become clear:
Couldn't match type `a0' with `a'
because type variable `a' would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: FooClass a = a - Int
The following variables have types that mention a0
fn :: a0 - Int (bound at /tmp/h.hs:16:16)
In the first argument of `FaI', namely `fn'
In the first argument of `foo', namely `(FaI fn)'
When we apply FaI to fn, the type-checker must ensure that fn is
really polymorphic. That is, free type variable in fn's type do not
occur elsewhere type environment: see the generalization rule in the
HM type system. When we removed the wrapper
unFaIntFn, we instantiated the quantified type variable a with some
specific (but not yet determined) type a0. The variable fn receives
the type fn:: a0 - Int. To type-check FaI fn, the type checker should
apply this rule
G |- fn :: FooClass a0 = a0 - Int
---
G |- FaI fn :: FaI
provided a0 does not occur in G. But it does occur: G has the binding
for fn, with the type a0 - Int, with the undesirable occurrence of
a0.
To solve the problem then, we somehow need to move this problematic binding fn
out of G. That binding is introduced by the pattern-match. So, we
should move the pattern-match under the application of FaI:
bar x = foo (FaI (case unFaIntFn x of IntFn fn - fn))
giving us the solution already pointed out.
So my next question is: why does unpacking the newtype via pattern
matching suddenly limit it to a single monomorphic type?
Because that's what removing wrappers like FaI does. There is no way
around it. That monomorphic type can be later generalized again, if
the side-condition for the generalization rule permits it.
You might have already noticed that `FaI' is like big Lambda of System
F, and unFaI is like System F type application. That's exactly what
they are:
http://okmij.org/ftp/Haskell/types.html#some-impredicativity
My explanation is a restatement of the Simon Peyton-Jones explanation,
in more concrete, Haskell terms.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
On 8/22/12 5:23 PM, Matthew Steele wrote: So my next question is: why does unpacking the newtype via pattern matching suddenly limit it to a single monomorphic type? Some Haskell code: foo :: (forall a. a - Int) - Bool foo fn = ... newtype IntFn a = IntFn (a - Int) bar1 :: (forall a. IntFn a) - Bool bar1 ifn = case ifn of IntFn fn - foo fn bar2 :: (forall a. IntFn a) - Bool bar2 ifn = foo (case ifn of IntFn fn - fn) Some (eta long) System Fc code it gets compiled down to: bar1 = \ (ifn :: forall a. IntFn a) - let A = ??? in case ifn @A of IntFn (fn :: A - Int) - foo (/\B - \(b::B) - fn @B b) bar2 = \ (ifn :: forall a. IntFn a) - foo (/\A - \(a::A) - case ifn @A of IntFn (fn :: A - Int) - fn a) There are two problems with bar1. First, where do we magic up that type A from? We need some type A. We can't just pattern match on ifn--- because it's a function (from types to terms)! Second, if we instantiate ifn at A, then we have that fn is monomorphic at A. But that means fn isn't polymorphic, and so we can't pass it to foo. Now, be careful of something here. The reason this fails is because we're compiling Haskell to System Fc, which is a Church-style lambda calculus (i.e., it explicitly incorporates types into the term language). It is this fact of being Church-style which forces us to instantiate ifn before we can do case analysis on it. If, instead, we were compiling Haskell down to a Curry-style lambda calculus (i.e., pure lambda terms, with types as mere external annotations) then everything would work fine. In the Curry-style world we wouldn't need to instantiate ifn at a specific type before doing case analysis, so we don't have the problem of magicking up a type. And, by parametricity, the function fn can't do anything particular based on the type of its argument, so we don't have the problem of instantiating too early[1]. Of course, (strictly) Curry-style lambda calculi are undecidable after rank-2 polymorphism, and the decidability at rank-2 is pretty wonky. Hence the reason for preferring to compile down to a Church-style lambda calculus. There may be some intermediate style which admits your code and also admits the annotations needed for inference/checking, but I don't know that anyone's explored such a thing. Curry-style calculi tend to be understudied since they go undecidable much more quickly. [1] I think. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Rigid skolem type variable escaping scope
While working on a project I have come across a new-to-me corner case of the
type system that I don't think I understand, and I am hoping that someone here
can enlighten me.
Here's a minimal setup. Let's say I have some existing code like this:
{-# LANGUAGE Rank2Types #-}
class FooClass a where ...
foo :: (forall a. (FooClass a) = a - Int) - Bool
foo fn = ...
Now I want to make a type alias for these (a - Int) functions, and give myself
a new way to call foo. I could do this:
type IntFn a = a - Int
bar :: (forall a. (FooClass a) = IntFn a) - Bool
bar fn = foo fn
This compiles just fine, as I would expect. But now let's say I want to change
it to make IntFn a newtype:
newtype IntFn a = IntFn (a - Int)
bar :: (forall a. (FooClass a) = IntFn a) - Bool
bar (IntFn fn) = foo fn
I had expected this to compile too. But instead, I get an error like this one
(using GHC 7.4.1):
Couldn't match type `a0' with `a'
because type variable `a' would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: FooClass a = a - Int
The following variables have types that mention a0
fn :: a0 - Int (bound at the line number that implements bar)
In the first argument of `foo', namely `fn'
In the expression: foo fn
In an equation for `bar': bar (IntFn fn) = foo fn
I don't think I am grasping why adding the layer of newtype
wrapping/unwrapping, without otherwise changing the types, introduces this
problem. Seems to me like the newtype version would also be type-safe if GHC
allowed it (am I wrong?), and I'm failing to understand why GHC can't allow it.
Is there a simple explanation, or else some reading that someone could point
me to? (-:
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
| This compiles just fine, as I would expect. But now let's say I want | to change it to make IntFn a newtype: | | newtype IntFn a = IntFn (a - Int) | | bar :: (forall a. (FooClass a) = IntFn a) - Bool | bar (IntFn fn) = foo fn The easiest way is to imagine transforming the function to System F. I'll ignore the (FooClass a) bit since it's irrelevant. We'd get bar = \(x :: forall a. IntFn a). ...what?... We can't do case-analysis on x; it has a for-all type, so we must instantiate it. But at what type? Let's guess some random type 'b': bar = \(x : forall a. IntFn a). case (x b) of IntFn (f :: b - Int) - foo f But now we are in trouble. 'foo' itself needs an argument of type (forall a. a-Int). So we need a big lambda bar = \(x : forall a. IntFn a). case (x b) of IntFn (f :: b - Int) - foo (/\a. f) But this is obviously wrong because 'b' escapes the /\a. I don't know if I can explain it better than that Simon | | I had expected this to compile too. But instead, I get an error like | this one (using GHC 7.4.1): | | Couldn't match type `a0' with `a' | because type variable `a' would escape its scope | This (rigid, skolem) type variable is bound by | a type expected by the context: FooClass a = a - Int | The following variables have types that mention a0 | fn :: a0 - Int (bound at the line number that implements bar) | In the first argument of `foo', namely `fn' | In the expression: foo fn | In an equation for `bar': bar (IntFn fn) = foo fn | | I don't think I am grasping why adding the layer of newtype | wrapping/unwrapping, without otherwise changing the types, introduces | this problem. Seems to me like the newtype version would also be type- | safe if GHC allowed it (am I wrong?), and I'm failing to understand why | GHC can't allow it. Is there a simple explanation, or else some | reading that someone could point me to? (-: | | Cheers, | -Matt | | | ___ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
Quoting Matthew Steele mdste...@alum.mit.edu:
{-# LANGUAGE Rank2Types #-}
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
In case you hadn't yet discovered it, the solution here is to unpack
the IntFn a bit later in a context where the required type argument is
known:
bar ifn = foo (case ifn of IntFn fn - fn)
Hope this helps.
Lauri
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:
Quoting Matthew Steele mdste...@alum.mit.edu:
{-# LANGUAGE Rank2Types #-}
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
In case you hadn't yet discovered it, the solution here is to unpack the
IntFn a bit later in a context where the required type argument is known:
bar ifn = foo (case ifn of IntFn fn - fn)
Hope this helps.
Ah ha, thank you! Yes, this solves my problem.
However, I confess that I am still struggling to understand why unpacking
earlier, as I originally tried, is invalid here. The two implementations are:
1) bar ifn = case ifn of IntFn fn - foo fn
2) bar ifn = foo (case ifn of IntFn fn - fn)
Why is (1) invalid while (2) is valid? Is is possible to make (1) valid by
e.g. adding a type signature somewhere, or is there something fundamentally
wrong with it? (I tried a few things that I thought might work, but had no
luck.)
I can't help feeling like maybe I am missing some small but important piece
from my mental model of how rank-2 types work. (-: Maybe there's some paper
somewhere I need to read?
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
On Wed, Aug 22, 2012 at 10:13 PM, Matthew Steele mdste...@alum.mit.edu wrote:
On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:
Quoting Matthew Steele mdste...@alum.mit.edu:
{-# LANGUAGE Rank2Types #-}
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
In case you hadn't yet discovered it, the solution here is to unpack the
IntFn a bit later in a context where the required type argument is known:
bar ifn = foo (case ifn of IntFn fn - fn)
Hope this helps.
Ah ha, thank you! Yes, this solves my problem.
However, I confess that I am still struggling to understand why unpacking
earlier, as I originally tried, is invalid here. The two implementations are:
1) bar ifn = case ifn of IntFn fn - foo fn
2) bar ifn = foo (case ifn of IntFn fn - fn)
Why is (1) invalid while (2) is valid? Is is possible to make (1) valid by
e.g. adding a type signature somewhere, or is there something fundamentally
wrong with it? (I tried a few things that I thought might work, but had no
luck.)
I can't help feeling like maybe I am missing some small but important piece
from my mental model of how rank-2 types work. (-: Maybe there's some paper
somewhere I need to read?
Look at it this way: the argument ifn has a type that says that *for
any type a you choose* it is an IntFn. But when you have unpacked it
by pattern matching, it only contains a function (a - Int) for *one
specific type a*. At that point, you've chosen your a.
The function foo wants an argument that works for *any* type a. So
passing it the function from IntFn isn't enough, since that only works
for *one specific a*. So you pass it a case expression that produces a
function for *any a*, by unpacking the IntFn only inside.
I hope that makes sense (and is correct...)
Erik
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
Quoting Matthew Steele mdste...@alum.mit.edu: 1) bar ifn = case ifn of IntFn fn - foo fn 2) bar ifn = foo (case ifn of IntFn fn - fn) I can't help feeling like maybe I am missing some small but important piece from my mental model of how rank-2 types work. As SPJ suggested, translation to System F with explicit type applications makes the issue clearer: 1) bar = \(ifn :: forall a. IntFn a). case ifn _a of IntFn (fn :: _a - Int) - foo (/\a. ???) 2) bar = \(ifn :: forall a. IntFn a). foo (/\a. case ifn a of IntFn (fn :: a - Int) - fn) Lauri ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
On Aug 22, 2012, at 4:32 PM, Erik Hesselink wrote:
On Wed, Aug 22, 2012 at 10:13 PM, Matthew Steele mdste...@alum.mit.edu
wrote:
On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:
Quoting Matthew Steele mdste...@alum.mit.edu:
{-# LANGUAGE Rank2Types #-}
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
In case you hadn't yet discovered it, the solution here is to unpack the
IntFn a bit later in a context where the required type argument is known:
bar ifn = foo (case ifn of IntFn fn - fn)
Hope this helps.
Ah ha, thank you! Yes, this solves my problem.
However, I confess that I am still struggling to understand why unpacking
earlier, as I originally tried, is invalid here. The two implementations
are:
1) bar ifn = case ifn of IntFn fn - foo fn
2) bar ifn = foo (case ifn of IntFn fn - fn)
Why is (1) invalid while (2) is valid? Is is possible to make (1) valid by
e.g. adding a type signature somewhere, or is there something fundamentally
wrong with it? (I tried a few things that I thought might work, but had no
luck.)
I can't help feeling like maybe I am missing some small but important piece
from my mental model of how rank-2 types work. (-: Maybe there's some
paper somewhere I need to read?
Look at it this way: the argument ifn has a type that says that *for
any type a you choose* it is an IntFn. But when you have unpacked it
by pattern matching, it only contains a function (a - Int) for *one
specific type a*. At that point, you've chosen your a.
The function foo wants an argument that works for *any* type a. So
passing it the function from IntFn isn't enough, since that only works
for *one specific a*. So you pass it a case expression that produces a
function for *any a*, by unpacking the IntFn only inside.
Okay, that does make sense, and I can see now why (2) works while (1) doesn't.
So my next question is: why does unpacking the newtype via pattern matching
suddenly limit it to a single monomorphic type? As you said, ifn has the type
something that can be an (IntFn a) for any a you choose. Since an (IntFn a)
is just a newtype around an (a - Int), why, when you unpack ifn into (IntFn
fn), is the type of fn not something that can be an (a - Int) for any a you
choose? Is it possible to add a local type annotation to force fn to remain
polymorphic?
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
