[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-cafe
Subject:    Re: [Haskell-cafe] Enforcing data structures invariant in the type system
From:       Nicola Gigante <nicola.gigante () gmail ! com>
Date:       2015-03-31 16:46:08
Message-ID: 51641C42-B65C-46CC-8387-3501AF0A63EE () gmail ! com
[Download RAW message or body]


> Il giorno 31/mar/2015, alle ore 15:41, Richard Eisenberg <eir@cis.upenn.edu> ha \
> scritto: 
> I thought I'd weigh in here, as my dissertation is all about how to encoding \
> invariants into Haskell's type system better. Here are some reactions to this \
> thread: 

Hi! is you dissertation available somewhere (or is still work in progress)?

> - In my opinion, Haskell is very capable of expressing invariants in its type \
> system today -- you don't need to go to Idris or Agda to get there. In certain \
> cases, this encoding can be quite natural and unobtrusive, and sometimes easier to \
> work with than in full-on dependently typed languages. The problem is that it's \
> very hard for a beginner in this space to tell which invariants are easy to encode \
> and which are hard. The red-black tree example is a great one for an \
> "easy-to-encode" invariant. The "Hasochism" paper [1] shows another. On the other \
> hand, my two (successful) attempts at "proving" a sorting algorithm correct are \
> very painful (insertion sort [2] and merge sort [3]). I'm sure one component in the \
> difference in level of elegance is that Conor and Sam are better dependently-typed \
> programmers than I am! 
> [1]: https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf
> [2]: https://github.com/goldfirere/singletons/blob/master/tests/compile-and-dump/InsertionSort/InsertionSortImp.hs
>  [3]: https://github.com/goldfirere/nyc-hug-oct2014/blob/master/OrdList.hs
> 

Very useful material, thanks!

> - The `singletons` package [4], can be helpful in doing dependently typed \
> programming in Haskell, and is cited in references previously mentioned in this \
> thread. But I wouldn't rely on it too much -- once you need lots of singletons \
> (more than, say, for numbers and Bools), your code will get very bogged down. It's \
> either time to come up with a different way of encoding for your invariant, give up \
> on compile-time verification, or switch to Idris. 
> [4]: http://hackage.haskell.org/package/singletons
> 
I have still to grasp where singletons are required and when they aren’t. 
The paper you linked above helps somehow.

> - The error messages are verbose. Haskell really needs a more interactive mode for \
> dependently typed programming! I'll answer one oft-answered question here: A \
> "skolem" is just a *bound* type variable. This is different from other type \
> variables GHC uses during type inference, which are free, *unification* type \
> variables. The point of a unification variable is as a placeholder until GHC \
> figures out the right type. A skolem variable is one that is actually bound in the \
> source code. Here's a tiny example: 
> > data Exists where
> > MkE :: forall a. a -> Exists
> > 
> > foo :: Exists -> Bool
> > foo (MkE x) = not x
> 
> This reports an error about a skolem(*) variable a not being Bool. Of course, we \
> can't know, in the body of `foo`, that the type of `x` is `Bool` -- `x` has type \
> `a`, for some unknown `a`. In this case `a` is a skolem. 
> (*): Sadly, the error message (in 7.8.3) just says "rigid" without "skolem". But \
> the choice of words in the error message is a little capricious, and other similar \
> cases can say "skolem”. 
Thank you for the explaination! 

> - Liquid Haskell goes a very different way than do all of the approaches above. It \
> uses a tool, called an SMT solver, outside of GHC to verify annotations in code. \
> Currently, Liquid Haskell can verify conditions that other approaches can only \
> dream of, including in Agda and Idris. (In particular, LH is very good around \
> integers, something that is otherwise a challenge to reason about in types.) But, \
> LH has two key limitations:  1) It reasons only about refinement types, which are \
> restrictions on existing types. Examples are "odd integers", "lists of Bools with \
> either 2 or 3 elements", "integers equal to 42", and "an integer `y` that is bigger \
> than that other integer `x`". Often, this is exactly what you want. But sometimes \
> it's not. 2) Its power is limited by the solving power of the attached SMT solver. \
> SMT solvers can reason about a lot, but -- of course -- they can't do everything. \
> If the SMT solver can't figure out your code, it's very hard to know what to do to \
> make things work again. However, this rarely comes up in practice. 
> I, personally, look forward to a future (years away) where we can have full \
> dependent types that also use an SMT solver. This will make the easy things easy, \
> but the hard things possible. 

That would be an interesting future without doubts!

> Richard

Thank you very much,
Nicola
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


[prev in list] [next in list] [prev in thread] [next in thread]