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

15 Sep 2014

      On Mon, 15 Sep 2014, Andras Slemmer <0slemi0@gmail.com> wrote:
...
-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.
So, now we have not only S, K, I, as Turing machine components,
but also Eval with its supporting instruction set.

ad checking vs inference: I will think about this.

ad UndecidableInstances: The two Turing machine realizations
offer evidence that one should not be naive about believing in
"Ex Falso, quodlibet.".  Part of the propaganda for Haskell goes like so:

   "Haskell has a rigorous compile time type checker which catches
   a certain kind of bug, and catches every one of this kind!
   (assuming a bugless Haskell compiler)."

But S, K, I and Eval show that, if one takes "Ex Falso,
quodlibet." too seriously, this cannot be true.  It cannot be
true, because once one invokes the Greater Options, the Universal
Machine is summoned, whether your program realizes an instance of
it or not.  Then, according to the Ancient Books of
Logic^W^W^W^W^Wmany recent textbooks, by "Ex Falso, quodlibet.", the
mere summoning, by internal over-pressure, explodes the type
checker, taking everything with it.  But of course this is not
true.  This should be enough to make the Wikipedia editors take
Carl Hewitt back!

   http://irobust.org
   [Above is a Google Doc, oi]

oo--JS.
...
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