Re: [Haskell-cafe] Hello and type-level SKI

-XUndecidableInstances gives it away in its name. Neither type checking or inference is decidable if you turn this extension on. It lifts some serious restrictions from type classes and type families that normally ensure that constraint computation/type functions normalise. I have also written a "proof" of turing completeness of UndecidableInstances a while ago: https://github.com/exFalso/TypeRegister This implements register machines in the type system, which are known to be turing complete. There are a few examples at the bottom, including an infinite loop. If you load it up in ghci and say (1 :: Inf) - which is just checking the type - it will stack overflow. On 14 September 2014 18:51, Jay Sulzberger wrote:

On Sun, 14 Sep 2014, Jay Sulzberger wrote:

...

On Fri, 12 Sep 2014, Tikhon Jelvis 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" wrote:

...

On Fri, Sep 12, 2014 at 7:25 PM, Jay Sulzberger 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@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

_______________________________________________ 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