[Haskell-cafe] Hello and type-level SKI

[Jay Sulzberger]

On Tue, 16 Sep 2014, Jay Sulzberger wrote:

>
> On Tue, 16 Sep 2014, Andras Slemmer <0slemi0 at 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 <jays at panix.com> wrote:
>> 
>>> 
>>> 
>>> 
>>> On Sat, 13 Sep 2014, Tslil Clingman <tslil.clingman at gmail.com> 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 at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>> 
>> 
>
>