[Haskell-cafe] Hello and type-level SKI

[Jay Sulzberger]

On Mon, 15 Sep 2014, Jay Sulzberger wrote:

>
>
>
> On Mon, 15 Sep 2014, Andras Slemmer <0slemi0 at 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.

Thanks, Andras!  Indeed here is what we get:

<blockquote
   what="demonstration of a register machine program running
         inside the Haskell type checker"
   see="https://raw.githubusercontent.com/exFalso/TypeRegister/master/register.hs
        for a copy of register.hs by Andras Slemmer"
   date="Monday 15 September 2014 17:29:17 -0400">

GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :load "register.hs"
[1 of 1] Compiling Main             ( register.hs, interpreted )
Ok, modules loaded: Main.
*Main> (1 :: Inf)

<interactive>:5:2:
     Context reduction stack overflow; size = 201
     Use -fcontext-stack=N to increase stack size to N
       Eval
         ((':) * (RP * * Zero Zero) ('[] *) :!: Zero)
         ((':) * (RP * * Zero Zero) ('[] *))
         (Update uf1 Zero (Succ *))
       ~ uf0
     In the expression: (1 :: Inf)
     In an equation for `it': it = (1 :: Inf)
*Main>

</blockquote>

oo--JS.


  < nothing new in stuff below />
>
> 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 <jays at panix.com> wrote:
>> 
>>> 
>>> 
>>> 
>>> 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
>>>>>> 
>>>>>> 
>>>>>> 
>>>>> 
>>>>
>>>>  _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>> 
>> 
>
>