Refinement types in Haskell as a library

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

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

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)

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-Fu...) and hence in ["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_t...), there at least exists "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_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 :)

Refinement types in Haskell as a library (nikita-volkov.github.io)

11 comments