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 <mdste...@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@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