[Haskell-cafe] Hello and type-level SKI

[Jay Sulzberger]

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.



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