Automated reasoning in F#, Scala, Haskell, C++, and Julia(phdp.github.io)

134 pointsby Bognar11 anni fa32 comments

phdp.github.io

Automated reasoning in F#, Scala, Haskell, C++, and Julia

http://phdp.github.io/posts/2015-04-05-automated-reasoning.html

14 comments

If anyone's interested in more examples, I have a complete F# port of the example code from The Handbook of Practical Logic and Automated Reasoning I did a while back with a couple of other F# devs: https://github.com/jack-pappas/fsharp-logic-examples

yummyfajitas11 anni fa

One neat feature which you can do in Scala (and probably C++), but which is probably more difficult in other languages, is impose constraints at the type level which force the underlying algebraic expression to already be (partially) simplified.

Suppose we represented Add instead as:

    case class Add(exprs: NonEmptyList[Expr with NotAdd]) extends Expr
    case class Const(value: Int) extends Expr with NotAdd
    case class ... extends Expr with NotAdd

Now nested Add's are a compile time error, and your expressions are automatically simpler. I'm not sure how easy this is to do in a language without subtypes.

I imagine it could be implemented with typeclasses in Haskell somehow (probably using existential types), but I doubt it would be as easy. (Any Haskell gurus care to comment?)

To see a more detailed illustration of how it would work, consider this free boolean algebra implementation: https://github.com/wingify/Oldmonk/blob/master/src/main/scal...

tikhonj11 anni fa

This feels like something you could do with GADTs in Haskell and OCaml. Here's your example rendered with GADTs:

    {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

    data IsAdd = IsAdd | NotAdd

    data Expr :: IsAdd -> * where
      Add   :: [Expr 'NotAdd] -> Expr 'IsAdd
      Const :: Integer        -> Expr 'NotAdd
      ...                     -> Expr 'NotAdd

You could also use True and False instead of Add and IsAdd, or even type-level string literals as arbitrary symbols:

    data Expr :: Symbol -> * where
      Add   :: [Expr "NotAdd"] -> Expr "IsAdd"
      Const :: Integer         -> Expr "NotAdd"

seliopou11 anni fa

Something like this could be implemented in Haskell or OCaml using GADTs[0]. You can add a phantom type parameter to the expression type and use that indicate whether or not the expression is well-formed according to some predicate--in your example, "non-nested added-ness." In fact this technique is often used as an introductory example to the use of GADTs, except the well-formed-ness property that's typically presented is that the expression is well-typed.

It's possible to express multiple properties using the same phantom type parameter is both languages. However, as you sort of alluded to, this encoding is much simpler if your language supports subtyping. Since OCaml does support subtyping, you can use polymorphic variants[1] for this purpose. For example, if you had the NotAdd property as well as the NotMult property, you could write down the type for an operation that depends on just the NotAdd operation like this:

    val notAddOp : ([> `NotAdd] as 'a) expr -> 'a t

... and write down an operation that depends on both like this:

    val bothOp : ([> `NotAdd | `NotMult] as 'a) expr -> 'a u

In Haskell, things would get more complicated. The type of the first operation would like more like this:

    notAddOp : Contains NotAdd a -> Expr a -> T a

... where the first argument is acting like a proof witness that the type parameter 'a in some sense "contains" tye type NotAdd. Similarly again for the second, except with two witnesses:

    bothOp : Contains NotAdd a -> Contains NotMult a -> Expr a -> T a

I haven't thought it completely through, but I'm almost certain that a combination of type classes and GCH extensions would allow you to turn those proof witness arguments into type class contexts.

Anyways, doing this sort of encoding of properties in types is all well and good until you start considering more realistic examples. Even in the one you presented, it's going to cause you problems if, say, you want to write an inliner for your language. Substituting an expression for a variable within a "NotAdd" addition may very well break the "NotAdd" property. This means that your inliner has to be aware of that property, so that it can preserve it while doing its job. In other words, the option of writing code that will break an invariant, and then immediately recover the invariant, is no longer on the table when you take this approach to verifying the correctness of your code. That may seem bad, until you try to verifiably balanced red-black tree without learning Coq and reading this[2].

Life's full of trade-offs.

[0]: https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ...

[1]: https://realworldocaml.org/v1/en/html/variants.html#polymorp...

[2]: http://www.cs.princeton.edu/~appel/papers/redblack.pdf

yummyfajitas11 anni fa

An inliner might break NotAdd, but why would it need to preserve it? Presumably an inliner is meant to be a homomorphism, not an isomorphism - i.e., it only goes one way.

Also, FreeBool[A] (the example given) actually handles substitution quite well. The `flatMap` operation will properly flatten things out:

     And(A,B,C).flatMap(C => D & E) = AND(A,B,D,E)

Yes, the compiler did help me get that right.

seliopou11 anni fa

If you're not careful about how you encode a property, the type system will _require_ you to preserve that property throughout each step of the computation, regardless of what sort of morphism that computation is. (It's an endomorphism.) Now that may be simple and straightforward when dealing with structural recursion over a boolean language, but if you want to write an inliner for Haskell, for example, it's probably a better idea to drop invariants from types (but not from the computation, of course), run the algorithm, and reintroduce invariants to the types afterwards.

Again, that example's way overshooting the complexity needed to prove the point. Even a seemingly simple invariant like the red-black balancing property is one that is impractical to preserve in this fashion without a proof assistant. And even then its practicality is still dubious.

steego11 anni fa

I know it's outside the scope of this post, but I'd like to add that F# adds a really nice feature called Active Patterns which are incredibly handy when your expression tree and logic become more complicated.

In the author's example, he matches on a few rules. A zero rule, an identity rule, an evaluation rule, and the default like so:

    let simplify1 e =
        match e with
        | Add (Const 0, x)
        | Add (x, Const 0)
        | Mul (x, Const 1)
        | Mul (Const 1, x)        -> x
        | Mul (x, Const 0)
        | Mul (Const 0, x)        -> Const 0
        | Add (Const a, Const b)  -> Const (a + b)
        | Mul (Const a, Const b)  -> Const (a * b)
        | _                       -> e

Active Patterns let you define these patterns as reusable blocks like so:

    let (|IdentityExpr|_|) = function
        | Add (Const 0, x)
        | Add (x, Const 0)
        | Mul (x, Const 1)
        | Mul (Const 1, x)        -> Some(x)
        | x -> None

It has the effect of making your pattern matching code more readable with a syntax that somewhat resembles a Prolog horn clause. As a bonus, you can mix and match these patterns when doing advanced reasoning.

    let simplify1 e =
        match e with
        | IdentityExpr(x) -> x
        | ZeroExpr()      -> 0
        | ConstantExpr(expr) -> Const(eval expr)
        | _                       -> e

junkyarddog11 anni fa

Have to agree that Active Patterns are an incredibly useful F# feature.

stuhood11 anni fa

In scala, the body of a match expression is a PartialFunction, and PartialFunctions compose similarly.

bryanjos11 anni fa

I enjoyed that post so much, I took a couple of minutes and made an Elixir version https://github.com/bryanjos/arithmetic.

The book is pretty expensive, but I want to get a copy.

one-more-minute11 anni fa

It's also worth checking out Julia's Match.jl package for more Haskell/OCaml-like pattern matching:

https://matchjl.readthedocs.org/en/latest/

bargl11 anni fa

Was the text at the bottom hidden for anybody other then me? I had to highlight it to see it. It seemed like a Easter egg, but I'm not sure.

It was below "Sum types and pattern matching are awesome."

jaytaylor11 anni fa

Nice find! How did you catch that?

bargl11 anni fa

I wish I had a cool answer but it was just an accident.

bglusman11 anni fa

Was also hidden for me, agree, small funny easter egg

phdpqc11 anni fa

Yes, it is an Easter egg. I thought it would take more time for people to notice. How well :P

harperlee11 anni fa

Perhaps it is an easy way to detect copies of the article...

cwyers11 anni fa

I loved the post, but I will say it's incredibly frustrating to see an interesting book referenced, to go looking for the book and to find that a USED copy on Amazon goes for $130.

profquail11 anni fa

It's also available on Safari Books if you have a subscription (e.g., through your workplace).

I agree, it's a pricy book though.

cwyers11 anni fa

We don't, but it's not like it's something I couldn't ask for if there was enough value there, so that's good to know. (Although I don't think Safari works with any e-ink readers, certainly not my Kindle.)

[deleted]11 anni fa

brudgers11 anni fa

It's the sort of book that always makes me curious: Is it as awesome as its title suggests?

logicallee11 anni fa

simple logic dictates that if it weren't awesome it wouldn't sell used for $130. Curiosity alone or a few references in some article or wherever won't drive a used price that high!

cossatot11 anni fa

A few professors requiring it to be used in a class will certainly drive it up that high, combined with the limited printing done by academic publishers.

It's pretty common and pretty unfortunate...

eggy11 anni fa

More like it is old enough that what number of copies were printed are owned. I personally perceive value, and I am willing to buy in at certain prices for the pay-off in knowledge and convenience. For instance, driving to a college, spending umpteen hours copying pages for a sub-standard replica of a book that I can have delivered for $130? I will buy it and do something else with the time saved. I was looking at buying an old Lisp book, 'Common LISP Modules: Artificial Intelligence in the Era of Neural Networks and Chaos Theory'. I already own a copy, but not where I am living for now. It was $3 on Amazon. There was a thread on HN where I mentioned the book, and the author himself wanted a copy, so he ordered it.

https://news.ycombinator.com/item?id=9877314

I checked back on Amazon, and it was over $80. Demand drove price. It is still on B&N for $86 right now:

http://www.barnesandnoble.com/w/common-lisp-modules-mark-wat...

seliopou11 anni fa

If you live close to a college or university, check to see if they have it. Almost all schools will let you into their libraries and let you browse (and photocopy) materials while you're there. Checking them out may be another issues, but you should ask about that while you're there as well.

semi-extrinsic11 anni fa

If you're frequently passing by a university library, see if they have a shelf where they sell old books. Mine does, and I've scored some sweet stuff there, e.g. Dunford and Schwartz' Linear Operators Part 1 & 2 together for $8, which looks to be $150 + shipping for used copies from Amazon ($400 new). As you can probably tell, there's an arb opportunity there as well.

paulkoer11 anni fa

If someone is wondering about the relationship between sum types (discriminated unions / case classes) and the visitor pattern, I've written about this here [1].

[1] http://paulkoerbitz.de/posts/Sum-Types-Visitors-and-the-Expr...

white-flame11 anni fa

This is constant propagation, probably one of the smallest slivers of "automated reasoning" that could arguably still be called as such. Personally, I don't think it falls under that umbrella. Could this get a title change?

mullr11 anni fa

Notably absent is anything in the lisp family, which excel at symbolic manipulation. Here's a Clojure version, both vanilla and with core.match.

https://gist.github.com/mullr/d655db18ebb7aa77a62e

barsonme11 anni fa

I got bored and wrote it in Go[1]. It's about as ugly as you'd expect.

[1] - https://gist.github.com/EricLagerg/beb586714cd9f509c812

cbsmith11 anni fa

The boost::variant example seems quite painful. I'd use boost::hana instead.

kaychaks11 anni fa

My attempt to port it in Erlang https://gist.github.com/kaychaks/61b9b860646a6a47375d

adamzubi70011 anni fa