4 ms·

I'm not very familiar with refinement types. How would that work? For example, how would you write a function that answers the mean value of an array of number

I'm not very familiar with refinement types. How would that work? For example, how would you write a function that answers the mean value of an array of numbers? You could define Array.Length to be of type NonNegativeInteger, but that still includes 0. Alternatively, you'd have to define a NonEmptyArray type that excludes arrays of length 0, but that seems less than useful.

rnhmjoj 10y ago
Yes, that's exactly how it works. See this article for an example: http://nikita-volkov.github.io/refined/ http://nikita-volkov.github.io/refined/ The thing is that, instead of redefining everything yourself, you could use a library that provides you with a set of predicates to compose and build the refinement you need. There are also much sophisticated ways to do this, like Liquid Haskell.
protomikron 10y ago
> Alternatively, you'd have to define a NonEmptyArray type that excludes arrays of length 0, but that seems less than useful. I think the usefulness of a specific NonEmptyArray type is controversial, and I would say such types could be extremely useful. AFAIK there have been discussions if Haskell's Prelude (part of the standard library providing a name space for convenient functions and types, similar to the functions you get in e.g. Python like map, zip, filter, range, etc.) should be more save by not advocating too generic types and functions like the standard `map`, `head` and `tail` implementations. Functions like `head` and `tail` can be seen as problematic as they can fail and cause runtime errors (the head and tail of an empty list cause a runtime error), but I do not think they already changed that (or if it's even a topic of discussion at the moment). It's a little bit a matter of taste. Think about Unix' "head" program that by default prints maximal 10 lines of a file. How should we deal with the following? $ touch empty.txt $ head -n1 empty.txt Currently this works - you do not get output and $? == 0, but one could also say "head" should panic here.
- mfukar 10y ago
  There no reason to "panic" about perfectly reasonable, valid use cases. `head` and `tail` in Haskell are badly designed (to address one of your examples), which is why every SO question about them and every question on haskell-beginners ends with the same answer: don't use them, pattern match instead.

rnhmjoj 10y ago

Yes, that's exactly how it works. See this article for an example: http://nikita-volkov.github.io/refined/ http://nikita-volkov.github.io/refined/ The thing is that, instead of redefining everything yourself, you could use a library that provides you with a set of predicates to compose and build the refinement you need. There are also much sophisticated ways to do this, like Liquid Haskell.

protomikron 10y ago

> Alternatively, you'd have to define a NonEmptyArray type that excludes arrays of length 0, but that seems less than useful. I think the usefulness of a specific NonEmptyArray type is controversial, and I would say such types could be extremely useful. AFAIK there have been discussions if Haskell's Prelude (part of the standard library providing a name space for convenient functions and types, similar to the functions you get in e.g. Python like map, zip, filter, range, etc.) should be more save by not advocating too generic types and functions like the standard `map`, `head` and `tail` implementations. Functions like `head` and `tail` can be seen as problematic as they can fail and cause runtime errors (the head and tail of an empty list cause a runtime error), but I do not think they already changed that (or if it's even a topic of discussion at the moment). It's a little bit a matter of taste. Think about Unix' "head" program that by default prints maximal 10 lines of a file. How should we deal with the following? $ touch empty.txt $ head -n1 empty.txt Currently this works - you do not get output and $? == 0, but one could also say "head" should panic here.

mfukar 10y ago
There no reason to "panic" about perfectly reasonable, valid use cases. `head` and `tail` in Haskell are badly designed (to address one of your examples), which is why every SO question about them and every question on haskell-beginners ends with the same answer: don't use them, pattern match instead.