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

34 pointsby nikita-volkov11 anni fa11 comments

nikita-volkov.github.io

Refinement types in Haskell as a library

http://nikita-volkov.github.io/refined/

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

dllthomas11 anni fa

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

nikita-volkov11 anni fa

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

nemo161811 anni fa

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

typish11 anni fa

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)

ics11 anni fa

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

CMCDragonkai11 anni fa

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

dllthomas11 anni fa

Precisely the difference between function application and function composition.

mijoharas11 anni fa

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

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

seanwilson11 anni fa

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-volkov11 anni fa

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