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-te... , 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".)