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

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