[Haskell-cafe] New type of ($) operator in GHC 8.0 is problematic
jo at durchholz.org
Tue Feb 9 22:55:29 UTC 2016
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.
, 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
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
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".)
More information about the Haskell-Cafe