4 ms·

Refinement types in Haskell as a library

34 points by nikita-volkov 11y ago

nemo1618 11y ago
Nice, but I was hoping for something like: slice :: Int{1..} -> [a] -> [[a]] slice n l = splitAt n l & \(a, b) -> a : slice n b I don't think this is possible in Haskell. Is there a language that supports this sort of syntax? (Also, what's up with that &? It doesn't seem to be a Prelude operator.)
- ics 11y ago
  Regarding &: https://www.fpcomplete.com/hoogle?q=%26&env=ghc-7.8-stable-14.09 https://www.fpcomplete.com/hoogle?q=%26&env=ghc-7.8-stable-1... If it's from lens, then it's "the flipped version of ($)".
  - mijoharas 11y ago
    There is a similar explanation if you search google for `haskell ampersand`[0] [0] http://qerub.se/ampersand http://qerub.se/ampersand
  - CMCDragonkai 11y ago
    What's the difference (&) and reverse function composition?
    - dllthomas 11y ago
      Precisely the difference between function application and function composition.
- typish 11y ago
  Liquid Haskell might be what you are looking for: http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf An example from that paper: type Nat = {v:Int | 0 <=v } type Pos = {v:Int | 0 < v } div :: Nat -> d:Pos -> {v:Nat | v <= n} The ATS programming language (http://www.ats-lang.org http://www.ats-lang.org) is more ML-like than Haskell-like but can have ranged integer types. Something like: fun slice {n:int | n >= 1} (a:int n, b:list)
- seanwilson 11y ago
  Dependently typed languages like DML, Epigram, ATS, Coq, Agda or Idris supports these kind of types. Unfortunately it quickly becomes difficult to work with this kind of typing when you introduce more complex properties.
- nikita-volkov 11y ago
  > Also, what's up with that &? It doesn't seem to be a Prelude operator. It's now in [Data.Function of "base"](http://hackage.haskell.org/package/base-4.8.0.0/docs/Data-Function.html#v:-38- http://hackage.haskell.org/package/base-4.8.0.0/docs/Data-Fu...) and hence in ["base-prelude"](http://hackage.haskell.org/package/base-prelude http://hackage.haskell.org/package/base-prelude).
mijoharas 11y ago
Can someone who knows more about haskell than me explain whether: 1. there are any disadvantages to using this library 2. there are any comparable libraries that I should/could be using instead (obviously with reasons as to why it's better/worse). because this sounds great and I now want to start using it everywhere!
- nikita-volkov 11y ago
  As it came up in the discussion at Reddit (http://www.reddit.com/r/haskell/comments/3425pk/refinement_types_as_a_library/cqqni9q http://www.reddit.com/r/haskell/comments/3425pk/refinement_t...), there at least exists "data-checked" (http://hackage.haskell.org/package/data-checked http://hackage.haskell.org/package/data-checked).
- dllthomas 11y ago
  Using the Template Haskell bits have all the disadvantages of Template Haskell - mostly a slower compile. Other than that, I don't see many downsides. As mentioned in the discussion on r/haskell, things get a little tricky when your arguments interact, but if you're okay with uncurrying you can still verify that you've got a sane combination: http://www.reddit.com/r/haskell/comments/3425pk/refinement_types_as_a_library/cqqik1i http://www.reddit.com/r/haskell/comments/3425pk/refinement_t... It also may require some explicit conversions in places they shouldn't strictly be necessary. Other than that, I don't see any downsides. There do seem to be a couple similar libraries, but feel free to start using it everywhere :)

34 points by nikita-volkov 11y ago

Nice, but I was hoping for something like: slice :: Int{1..} -> [a] -> [[a]] slice n l = splitAt n l & \(a, b) -> a : slice n b I don't think this is possible in Haskell. Is there a language that supports this sort of syntax? (Also, what's up with that &? It doesn't seem to be a Prelude operator.)

ics 11y ago
Regarding &: https://www.fpcomplete.com/hoogle?q=%26&env=ghc-7.8-stable-14.09 https://www.fpcomplete.com/hoogle?q=%26&env=ghc-7.8-stable-1... If it's from lens, then it's "the flipped version of ($)".
- mijoharas 11y ago
  There is a similar explanation if you search google for `haskell ampersand`[0] [0] http://qerub.se/ampersand http://qerub.se/ampersand
- CMCDragonkai 11y ago
  What's the difference (&) and reverse function composition?
  - dllthomas 11y ago
    Precisely the difference between function application and function composition.
typish 11y ago
Liquid Haskell might be what you are looking for: http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf An example from that paper: type Nat = {v:Int | 0 <=v } type Pos = {v:Int | 0 < v } div :: Nat -> d:Pos -> {v:Nat | v <= n} The ATS programming language (http://www.ats-lang.org http://www.ats-lang.org) is more ML-like than Haskell-like but can have ranged integer types. Something like: fun slice {n:int | n >= 1} (a:int n, b:list)
seanwilson 11y ago
Dependently typed languages like DML, Epigram, ATS, Coq, Agda or Idris supports these kind of types. Unfortunately it quickly becomes difficult to work with this kind of typing when you introduce more complex properties.
nikita-volkov 11y ago
> Also, what's up with that &? It doesn't seem to be a Prelude operator. It's now in [Data.Function of "base"](http://hackage.haskell.org/package/base-4.8.0.0/docs/Data-Function.html#v:-38- http://hackage.haskell.org/package/base-4.8.0.0/docs/Data-Fu...) and hence in ["base-prelude"](http://hackage.haskell.org/package/base-prelude http://hackage.haskell.org/package/base-prelude).

mijoharas 11y ago

Can someone who knows more about haskell than me explain whether: 1. there are any disadvantages to using this library 2. there are any comparable libraries that I should/could be using instead (obviously with reasons as to why it's better/worse). because this sounds great and I now want to start using it everywhere!

nikita-volkov 11y ago
As it came up in the discussion at Reddit (http://www.reddit.com/r/haskell/comments/3425pk/refinement_types_as_a_library/cqqni9q http://www.reddit.com/r/haskell/comments/3425pk/refinement_t...), there at least exists "data-checked" (http://hackage.haskell.org/package/data-checked http://hackage.haskell.org/package/data-checked).
dllthomas 11y ago
Using the Template Haskell bits have all the disadvantages of Template Haskell - mostly a slower compile. Other than that, I don't see many downsides. As mentioned in the discussion on r/haskell, things get a little tricky when your arguments interact, but if you're okay with uncurrying you can still verify that you've got a sane combination: http://www.reddit.com/r/haskell/comments/3425pk/refinement_types_as_a_library/cqqik1i http://www.reddit.com/r/haskell/comments/3425pk/refinement_t... It also may require some explicit conversions in places they shouldn't strictly be necessary. Other than that, I don't see any downsides. There do seem to be a couple similar libraries, but feel free to start using it everywhere :)