[Haskell-cafe] New type of ($) operator in GHC 8.0 is problematic

[Joachim Durchholz]

Am 09.02.2016 um 23:07 schrieb Marcin Mrotek:
>>
>> I feel that this is similar to expressing value constraints in the type
>> system, e.g. ranges or squareness of matrixes. Yes it can be done in
>> Haskell's type system, yes it does typecheck beautifully, but the type
>> declarations behind these kinds of feats will just make any ordinary
>> programmer go MEGO. Even the bright ones.
>> I conclude that the type system isn't the right place for that kind of
>> checking. To be understandable, such constraints need to be expressed as
>> boolean assertions, not as some inductive construct. YMMV
>
> Two words: refinement types.

Are these in Haskell already? I see them referenced in something that's 
called LiquidHaskell, which has its last blog entry from Jan 2015.

On 
http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/12/09/checking-termination.lhs/ 
, it is doing termination checks via handcrafted induction.
In functions, induction (i.e. standard recursion pattern) is handled 
using higher-order functions, where's the higher-order logic in the 
predicates?
And termination proofs shouldn't be implicit in the proof structure, I'd 
prefer a "terminates" predicate ("unlifted" if you will) on the function 
(not the function's type) which could be true, false, or of the form "if 
parameter x has properties A, B, and C, then the function is guaranteed 
to terminate", i.e. an implication.

Just off the top of my head where I see problems for the everyday 
programmer.
It's still interesting work. I hope somebody gets the funding to carry 
that to practical usefulness.

(Please answer to the list, CCing the list means I can't "reply to list".)