[Haskell-cafe] Hello and type-level SKI

[Jay Sulzberger]

On Sun, 14 Sep 2014, Jay Sulzberger wrote:

>
>
>
> On Fri, 12 Sep 2014, Tikhon Jelvis <tikhon at jelv.is> wrote:
>
>> Note how the provided code enables a bunch of language extensions, most
>> notably UndecidableInstances. (Yep, that's exactly what it sounds like!)
>> 
>> It's quite far removed from standard Haskell or full type inference.
>
> Yes.  One thing that I now know is that, to date, there is a
> clean separation of estimation of the type of a function from the
> next stage of the GHC pipeline.  In particular you cannot see in
> the Core code for the function the effect of the extensions,
> except possibly, whether or not any code is produced.
>
> I say "know", but all I have done is look at the high level
> explanations.  I have not looked at any compiler code.  So my
> understanding is not good and likely to be largely mistaken.
>
> oo--JS.

I should have in my first post distinguished "inference" from
"checking".  I believe checking is still decidable, but inference
no longer is, if you call GHC with given options.

oo--JS.


>
>
>> On Sep 12, 2014 4:30 PM, "Brandon Allbery" <allbery.b at gmail.com> wrote:
>> 
>>> On Fri, Sep 12, 2014 at 7:25 PM, Jay Sulzberger <jays at panix.com> wrote:
>>> 
>>>> But this is impossible!  The type system of Haskell can be
>>>> handled by a Hindley-Milner-Damas style type checker.  Such a
>>>> type checker always comes to a halt with a Yea or Nay answer.  So
>>>> one cannot get a simulation of the combinators S, K, I inside the
>>>> Haskell type system.
>>>> 
>>>> What have I misunderstood?  And, in case GHC really does now
>>>> handle stuff beyond the HMD horizon, what does the New Core
>>>> language look like?
>>>> 
>>> 
>>> Standard Haskell is (or was) H-M extended with typeclasses. GHC moved
>>> beyond that years ago; internally it's System Fw (
>>> http://en.wikipedia.org/wiki/System_F#System_F.CF.89), and its Core
>>> language reflects this.
>>> 
>>> --
>>> brandon s allbery kf8nh                               sine nomine
>>> associates
>>> allbery.b at gmail.com
>>> ballbery at sinenomine.net
>>> unix, openafs, kerberos, infrastructure, xmonad
>>> http://sinenomine.net
>>> 
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>> 
>>> 
>> 
>
>