Hello and type-level SKI

newer
Hackage package "synopsis" sections

Tslil Clingman

12 Sep 2014 12 Sep '14

4:56 p.m.

Greetings all, I've been reading this list for a short while and I thought I'd like to begin to contribute where possible. This message pretty much serves to say: - Hello, Haskell! - This community is great, and it's always been a great pleasure to read the newsgroup(s) - Here is a small and likely multiply re-re-discovered `proof' of why the type system is Turing Complete

...

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}

...

data S2 x y data S1 x data S data K1 x data K data I

...

class Apply a b c | a b -> c instance Apply K x (K1 x) instance Apply S x (S1 x) instance Apply (S1 x) y (S2 x y) instance Apply I x x instance Apply (K1 x) y x instance (Apply x z xz, Apply y z yz, Apply xz yz a) => Apply (S2 x y) z a

...

-- The core function apply :: (Apply a b c) => a -> b -> c apply _ _ = undefined -- Hereendeththelesson --

...

-- For `ease of use', but not strictly necessary data X data Y data Z s = undefined :: S k = undefined :: K i = undefined :: I x = undefined :: X y = undefined :: Y z = undefined :: Z -- Example reverse = apply (apply s (apply k (apply s i))) k

I just thought I'd share this snippet here, but if this is not the right place, or it's too long or something please don't hesitate to let me know. Thanks for your attention, Yours &c., Tslil

Attachments:

attachment.sig (application/pgp-signature — 818 bytes)

Show replies by date

Jay Sulzberger

12 Sep 12 Sep

7:25 p.m.

On Fri, 12 Sep 2014, Tslil Clingman wrote:

...

Greetings all,

I've been reading this list for a short while and I thought I'd like to begin to contribute where possible. This message pretty much serves to say:

- Hello, Haskell! - This community is great, and it's always been a great pleasure to read the newsgroup(s) - Here is a small and likely multiply re-re-discovered `proof' of why the type system is Turing Complete

...
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}

...
data S2 x y data S1 x data S data K1 x data K data I

...
class Apply a b c | a b -> c instance Apply K x (K1 x) instance Apply S x (S1 x) instance Apply (S1 x) y (S2 x y) instance Apply I x x instance Apply (K1 x) y x instance (Apply x z xz, Apply y z yz, Apply xz yz a) => Apply (S2 x y) z a

...
-- The core function apply :: (Apply a b c) => a -> b -> c apply _ _ = undefined -- Hereendeththelesson --

...
-- For `ease of use', but not strictly necessary data X data Y data Z s = undefined :: S k = undefined :: K i = undefined :: I x = undefined :: X y = undefined :: Y z = undefined :: Z -- Example reverse = apply (apply s (apply k (apply s i))) k

I just thought I'd share this snippet here, but if this is not the right place, or it's too long or something please don't hesitate to let me know.

Thanks for your attention, Yours &c., Tslil

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

Brandon Allbery

7:30 p.m.

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

Tikhon Jelvis

7:46 p.m.

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

Tslil Clingman

13 Sep 13 Sep

6:43 a.m.

Right, so to be fair a more accurate description would have been: `It can be shown that GHC with numerous extensions gives rise to a type system which is Turing Complete', my mistake. I certainly didn't mean to mislead anyone. All too often I conflate Haskell (2010 or so) and the capabilities of GHC -- this is a trap which ensnares many, I suspect. -- Yours &c., Tslil

Jay Sulzberger

15 Sep 15 Sep

10:37 p.m.

On Sat, 13 Sep 2014, Tslil Clingman wrote:

...

Right, so to be fair a more accurate description would have been: `It can be shown that GHC with numerous extensions gives rise to a type system which is Turing Complete', my mistake. I certainly didn't mean to mislead anyone.

All too often I conflate Haskell (2010 or so) and the capabilities of GHC -- this is a trap which ensnares many, I suspect.

-- Yours &c., Tslil

Dear Tslil, my exclamation was with tongue part way in cheek, so no worry as far as I am concerned. I do not know much about Haskell, and less about GHC, but I am slowly learning. I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output. My guess today is that that most of the time, no matter what extensions are invoked, if the source type-checks, then we get the same Core output. I am still smiling at your S, K, I, and Andras's Eval. oo--JS.

Andras Slemmer

16 Sep 16 Sep

1:26 p.m.

...

I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output.

Most extensions are safe, there are a few that are known to cause (or to have caused) trouble. Safe (type-system) extensions include: MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances, LiberalTypeSynonyms, DataKinds, ConstraintKinds, GADTs, ExistentialQuantification, RankNTypes, GeneralizedNewtypeDeriving(since ghc 7.8), TypeFamilies. I would also put UndecidableInstances here, as it will not produce incorrect code, it's just that the compiler may give up on type checking. There are a couple of more, this is just to give you an idea.. Safe but never to be used extensions(except if you know -exactly- what you're doing): OverlappingInstances, IncoherentInstances Unsafe extensions: GeneralizedNewtypeDeriving(before ghc 7.8), with which one was able to implement coerce :: a -> b Regarding inference: if a type is not inferable that doesn't mean the term in question is incorrect. For example if you switch on RankNTypes very simple terms can inhabit several types. For example take f = (\x -> x). You may think f must have type :: a -> a, but a completely different type, :: (forall a. a) -> b also works (although it's not very useful). On 16 September 2014 04:37, Jay Sulzberger wrote:

...

On Sat, 13 Sep 2014, Tslil Clingman wrote:

Right, so to be fair a more accurate description would have been: `It

...
can be shown that GHC with numerous extensions gives rise to a type system which is Turing Complete', my mistake. I certainly didn't mean to mislead anyone.

All too often I conflate Haskell (2010 or so) and the capabilities of GHC -- this is a trap which ensnares many, I suspect.

-- Yours &c., Tslil

Dear Tslil, my exclamation was with tongue part way in cheek, so no worry as far as I am concerned. I do not know much about Haskell, and less about GHC, but I am slowly learning. I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output. My guess today is that that most of the time, no matter what extensions are invoked, if the source type-checks, then we get the same Core output.

I am still smiling at your S, K, I, and Andras's Eval.

oo--JS.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Mateusz Kowalczyk

1:29 p.m.

On 09/16/2014 06:26 PM, Andras Slemmer wrote:

...

...
I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output.

Most extensions are safe, there are a few that are known to cause (or to have caused) trouble.

Safe (type-system) extensions include: MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances, LiberalTypeSynonyms, DataKinds, ConstraintKinds, GADTs, ExistentialQuantification, RankNTypes, GeneralizedNewtypeDeriving(since ghc 7.8), TypeFamilies. I would also put UndecidableInstances here, as it will not produce incorrect code, it's just that the compiler may give up on type checking. There are a couple of more, this is just to give you an idea..

Safe but never to be used extensions(except if you know -exactly- what you're doing): OverlappingInstances, IncoherentInstances

Unsafe extensions: GeneralizedNewtypeDeriving(before ghc 7.8), with which one was able to implement coerce :: a -> b

Regarding inference: if a type is not inferable that doesn't mean the term in question is incorrect. For example if you switch on RankNTypes very simple terms can inhabit several types. For example take f = (\x -> x). You may think f must have type :: a -> a, but a completely different type, :: (forall a. a) -> b also works (although it's not very useful).

I don't know if I'd put TypeFamilies on there today due to https://ghc.haskell.org/trac/ghc/ticket/9562

...

On 16 September 2014 04:37, Jay Sulzberger wrote:

...
On Sat, 13 Sep 2014, Tslil Clingman wrote:

Right, so to be fair a more accurate description would have been: `It

...
can be shown that GHC with numerous extensions gives rise to a type system which is Turing Complete', my mistake. I certainly didn't mean to mislead anyone.

All too often I conflate Haskell (2010 or so) and the capabilities of GHC -- this is a trap which ensnares many, I suspect.

-- Yours &c., Tslil

Dear Tslil, my exclamation was with tongue part way in cheek, so no worry as far as I am concerned. I do not know much about Haskell, and less about GHC, but I am slowly learning. I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output. My guess today is that that most of the time, no matter what extensions are invoked, if the source type-checks, then we get the same Core output.

I am still smiling at your S, K, I, and Andras's Eval.

oo--JS.

-- Mateusz K.

Andras Slemmer

1:57 p.m.

...

I don't know if I'd put TypeFamilies on there today due to https://ghc.haskell.org/trac/ghc/ticket/9562 Huh! you learn something everyday:D

On 16 September 2014 19:29, Mateusz Kowalczyk wrote:

...

On 09/16/2014 06:26 PM, Andras Slemmer wrote:

...
...
I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output.

Most extensions are safe, there are a few that are known to cause (or to have caused) trouble.

Safe (type-system) extensions include: MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances, LiberalTypeSynonyms, DataKinds, ConstraintKinds, GADTs, ExistentialQuantification, RankNTypes, GeneralizedNewtypeDeriving(since ghc 7.8), TypeFamilies. I would also put UndecidableInstances here, as it will not produce incorrect code, it's just that the compiler may give up on type checking. There are a couple of more, this is just to give you an idea..

Safe but never to be used extensions(except if you know -exactly- what you're doing): OverlappingInstances, IncoherentInstances

Unsafe extensions: GeneralizedNewtypeDeriving(before ghc 7.8), with which one was able to implement coerce :: a -> b

Regarding inference: if a type is not inferable that doesn't mean the term in question is incorrect. For example if you switch on RankNTypes very simple terms can inhabit several types. For example take f = (\x -> x). You may think f must have type :: a -> a, but a completely different type, :: (forall a. a) -> b also works (although it's not very useful).

I don't know if I'd put TypeFamilies on there today due to https://ghc.haskell.org/trac/ghc/ticket/9562

...
On 16 September 2014 04:37, Jay Sulzberger wrote:

...
On Sat, 13 Sep 2014, Tslil Clingman wrote:

Right, so to be fair a more accurate description would have been: `It

...
can be shown that GHC with numerous extensions gives rise to a type system which is Turing Complete', my mistake. I certainly didn't mean

to

...
...
mislead anyone.

All too often I conflate Haskell (2010 or so) and the capabilities of GHC -- this is a trap which ensnares many, I suspect.

-- Yours &c., Tslil

Dear Tslil, my exclamation was with tongue part way in cheek, so no worry as far as I am concerned. I do not know much about Haskell, and less about GHC, but I am slowly learning. I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output. My guess today is that that most of the time, no matter what extensions are invoked, if the source type-checks, then we get the same Core output.

I am still smiling at your S, K, I, and Andras's Eval.

oo--JS.

-- Mateusz K.

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Brandon Allbery

2:13 p.m.

On Tue, Sep 16, 2014 at 1:26 PM, Andras Slemmer <0slemi0@gmail.com> wrote:

...

Safe but never to be used extensions(except if you know -exactly- what you're doing): OverlappingInstances, IncoherentInstances

Are we sure that different parts of a program inferring different instances can't create at least a limited form of unsafeCoerce? -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Brandon Allbery

2:16 p.m.

On Tue, Sep 16, 2014 at 2:13 PM, Brandon Allbery wrote:

...

On Tue, Sep 16, 2014 at 1:26 PM, Andras Slemmer <0slemi0@gmail.com> wrote:

...
Safe but never to be used extensions(except if you know -exactly- what you're doing): OverlappingInstances, IncoherentInstances

Are we sure that different parts of a program inferring different instances can't create at least a limited form of unsafeCoerce?

...and I think the already mentioned ticket just confirmed that it's at least potentially possible via hs-boot files, although I was thinking of a slightly more "direct" mechanism. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Jay Sulzberger

5:54 p.m.

On Tue, 16 Sep 2014, Andras Slemmer <0slemi0@gmail.com> wrote:

...

...
I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output.

Most extensions are safe, there are a few that are known to cause (or to have caused) trouble.

Safe (type-system) extensions include: MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances, LiberalTypeSynonyms, DataKinds, ConstraintKinds, GADTs, ExistentialQuantification, RankNTypes, GeneralizedNewtypeDeriving(since ghc 7.8), TypeFamilies. I would also put UndecidableInstances here, as it will not produce incorrect code, it's just that the compiler may give up on type checking. There are a couple of more, this is just to give you an idea..

Safe but never to be used extensions(except if you know -exactly- what you're doing): OverlappingInstances, IncoherentInstances

Unsafe extensions: GeneralizedNewtypeDeriving(before ghc 7.8), with which one was able to implement coerce :: a -> b

Regarding inference: if a type is not inferable that doesn't mean the term in question is incorrect. For example if you switch on RankNTypes very simple terms can inhabit several types. For example take f = (\x -> x). You may think f must have type :: a -> a, but a completely different type, :: (forall a. a) -> b also works (although it's not very useful).

Thanks, Andras! OK, I have read further in the thread and now looked at https://ghc.haskell.org/trac/ghc/ticket/9562 and at http://www.haskell.org/haskellwiki/GHC/Type_families ad TypeFamilies: One may distinguish two kinds of extensions of a type inferencer/checker: 1. a pure syntactical sugar extension 2. an extension that modifies the type inferencer/checker A pure sugar extension works as follows: The source code is re-written and the re-written code is passed to the usual type inferencer/checker, from which point all proceeds same as before. An extension of kind 2 is a modification of the usual type inferencer/checker, which modified engine is then run. Of course there might be some source to source rewriting before running the modified engine. Question: Is TypeFamilies an extension of kind 1, or of kind 2? oo--JS.

...

On 16 September 2014 04:37, Jay Sulzberger wrote:

...
On Sat, 13 Sep 2014, Tslil Clingman wrote:

Right, so to be fair a more accurate description would have been: `It

...
can be shown that GHC with numerous extensions gives rise to a type system which is Turing Complete', my mistake. I certainly didn't mean to mislead anyone.

All too often I conflate Haskell (2010 or so) and the capabilities of GHC -- this is a trap which ensnares many, I suspect.

-- Yours &c., Tslil

Dear Tslil, my exclamation was with tongue part way in cheek, so no worry as far as I am concerned. I do not know much about Haskell, and less about GHC, but I am slowly learning. I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output. My guess today is that that most of the time, no matter what extensions are invoked, if the source type-checks, then we get the same Core output.

I am still smiling at your S, K, I, and Andras's Eval.

oo--JS.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Jay Sulzberger

10:20 p.m.

On Tue, 16 Sep 2014, Jay Sulzberger wrote:

...

On Tue, 16 Sep 2014, Andras Slemmer <0slemi0@gmail.com> wrote:

...
...
I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output.

Most extensions are safe, there are a few that are known to cause (or to have caused) trouble.

Safe (type-system) extensions include: MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances, LiberalTypeSynonyms, DataKinds, ConstraintKinds, GADTs, ExistentialQuantification, RankNTypes, GeneralizedNewtypeDeriving(since ghc 7.8), TypeFamilies. I would also put UndecidableInstances here, as it will not produce incorrect code, it's just that the compiler may give up on type checking. There are a couple of more, this is just to give you an idea..

Safe but never to be used extensions(except if you know -exactly- what you're doing): OverlappingInstances, IncoherentInstances

Unsafe extensions: GeneralizedNewtypeDeriving(before ghc 7.8), with which one was able to implement coerce :: a -> b

Regarding inference: if a type is not inferable that doesn't mean the term in question is incorrect. For example if you switch on RankNTypes very simple terms can inhabit several types. For example take f = (\x -> x). You may think f must have type :: a -> a, but a completely different type, :: (forall a. a) -> b also works (although it's not very useful).

Thanks, Andras!

OK, I have read further in the thread and now looked at

https://ghc.haskell.org/trac/ghc/ticket/9562

and at

http://www.haskell.org/haskellwiki/GHC/Type_families

ad TypeFamilies: One may distinguish two kinds of extensions of a type inferencer/checker:

1. a pure syntactical sugar extension

2. an extension that modifies the type inferencer/checker

A pure sugar extension works as follows:

The source code is re-written and the re-written code is passed to the usual type inferencer/checker, from which point all proceeds same as before.

An extension of kind 2 is a modification of the usual type inferencer/checker, which modified engine is then run. Of course there might be some source to source rewriting before running the modified engine.

Question: Is TypeFamilies an extension of kind 1, or of kind 2?

oo--JS.

OK, my guess after looking at the paper System F with Type Equality Coercions by M. Sulzmann et al pointed to on the page http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html is that GHC's type inferencer/checker is today different from what it was before TypeFamilies, and a few other recent faculties. In related news, Brent Abraham Yorgey has a version of his thesis "Combinatorial Species and Labelled Structures" available via: http://byorgey.wordpress.com/2014/08/10/readers-wanted/ oo--JS.

...

...
On 16 September 2014 04:37, Jay Sulzberger wrote:

...
On Sat, 13 Sep 2014, Tslil Clingman wrote:

Right, so to be fair a more accurate description would have been: `It

...
can be shown that GHC with numerous extensions gives rise to a type system which is Turing Complete', my mistake. I certainly didn't mean to mislead anyone.

All too often I conflate Haskell (2010 or so) and the capabilities of GHC -- this is a trap which ensnares many, I suspect.

-- Yours &c., Tslil

Dear Tslil, my exclamation was with tongue part way in cheek, so no worry as far as I am concerned. I do not know much about Haskell, and less about GHC, but I am slowly learning. I am still not sure how far modifications to the type inferencer/checker affect the code produced, beyond whether any code at all is output. My guess today is that that most of the time, no matter what extensions are invoked, if the source type-checks, then we get the same Core output.

I am still smiling at your S, K, I, and Andras's Eval.

oo--JS.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Jay Sulzberger

14 Sep 14 Sep

12:46 p.m.

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.

...

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

Jay Sulzberger

12:51 p.m.

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

Andras Slemmer

15 Sep 15 Sep

4:11 a.m.

-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

Jay Sulzberger

4:56 p.m.

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

Jay Sulzberger

5:30 p.m.

On Mon, 15 Sep 2014, Jay Sulzberger wrote:

...

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.

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 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

Gershom B

12 Sep 12 Sep

11:28 p.m.

On September 12, 2014 at 7:30:28 PM, Brandon Allbery (allbery.b@gmail.com) wrote:

...

On Fri, Sep 12, 2014 at 7:25 PM, Jay Sulzberger wrote:

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

It has now moved beyond that too and is system FC (https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/FC) which adds equality constraints and coercions. Also note that, as I understand it, typeclass constraints are dealt with in the typechecker, before core is generated. So if you use a terrible combination of features and instances and produce something at the type level that loops, then the typechecker just doesn’t terminate (well, it actually runs out of context stack typically…). You can find more details in the commentary (https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/HscMain) which now looks way clearer than last time I checked. -g

Jay Sulzberger

13 Sep 13 Sep

12:02 a.m.

On Fri, 12 Sep 2014, Gershom B wrote:

...

...
On September 12, 2014 at 7:30:28 PM, Brandon Allbery (allbery.b@gmail.com) wrote: On Fri, Sep 12, 2014 at 7:25 PM, Jay Sulzberger wrote:

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

It has now moved beyond that too and is system FC (https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/FC) which adds equality constraints and coercions.

Also note that, as I understand it, typeclass constraints are dealt with in the typechecker, before core is generated. So if you use a terrible combination of features and instances and produce something at the type level that loops, then the typechecker just doesn’t terminate (well, it actually runs out of context stack typically…). You can find more details in the commentary (https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/HscMain) which now looks way clearer than last time I checked.

-g

Thanks, Gershom! I just glanced at the page. I know that GHC is a serious compiler, but just the high level flow diagram impresses. The compiler deals with stuff more logically complex than the usual presentations of System FC deal with, such as "strictness". To think that sometimes it runs without dumping core, and even, I believe this part of Haskell propaganda, often produces correct programs, ah, well, I say MORE FUNDING and don't worry about success. oo--JS. PS. I just looked at https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/CoreSynType I am reassured.

Jay Sulzberger

12:06 a.m.

On Fri, 12 Sep 2014, 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.

Thanks, Brandon! OK, so the way one simulates, ridiculous word, a Turing machine is to write code for a function in Haskell. The (simulation of) running of the Turing machine, if I understand correctly, is Haskell's attempt to calculate a type for the function. Specifically, the type inferencer's attempt. I will look at the implementation of S, K, and I, and try to figure out how this works. oo--JS.

...

-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

3899

Age (days ago)

3904

Last active (days ago)

List overview

Download

20 comments

8 participants

participants (8)

Andras Slemmer
Brandon Allbery
Gershom B
Jay Sulzberger
Mateusz Kowalczyk
Tikhon Jelvis
Tslil Clingman
Tslil Clingman