Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-24 Thread Matthew Steele
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

Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-24 Thread Ryan Ingram
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 ~ ())

Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-23 Thread wren ng thornton
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 ::

Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-22 Thread Simon Peyton-Jones
| 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

Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-22 Thread Lauri Alanko
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)

Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-22 Thread Matthew Steele
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

Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-22 Thread Erik Hesselink
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

Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-22 Thread Lauri Alanko
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

Re: [Haskell-cafe] Rigid skolem type variable escaping scope

2012-08-22 Thread Matthew Steele
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 ...