[Haskell-cafe] Rigid skolem type variable escaping scope

[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 ~ ()) => T
f :: T a -> a
f T = ()

x :: T ()
x = T

C:\haskell>ghc -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 <mdsteele at alum.mit.edu>wrote:

> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120824/61e006e5/attachment.htm>