Refinement types in Haskell as a library | Hacker News Reader

Refinement types in Haskell as a library

nikita-volkov.github.io

34 pointsnikita-volkov11 comments

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!

As it came up in the discussion at Reddit (http://www.reddit.com/r/haskell/comments/3425pk/refinement_t...), there at least exists "data-checked" (http://hackage.haskell.org/package/data-checked).

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_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 :)

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.)

Regarding &: 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 ($)".

There is a similar explanation if you search google for `haskell ampersand`[0]

[0] http://qerub.se/ampersand

What's the difference (&) and reverse function composition?

Precisely the difference between function application and function composition.

Liquid Haskell might be what you are looking for: 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) 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)

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.

> 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-Fu...) and hence in ["base-prelude"](http://hackage.haskell.org/package/base-prelude).

Reply on news.ycombinator.com