[Haskell-cafe] Hello and type-level SKI

[Mateusz Kowalczyk]

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