#haskell15

FP encourages equational reasoning!

In Haskell, in practice: type class laws, RULES

Reasoning by hand: tedious! Easy to gloss over details without mechanical support. (So not done in practice)

HERMIT: interactive/scripted transformation on core

IDEA: add lemmas to HERMIT. Equivalences beween core expressions; support conjunction, disjunction, implication, quantification

Then redo KURE, transformations on lemmas, rather than on expressions.

Case study: type class laws, Pearls of Functional Algorithm Design

(ezyang: Soundness????)

Property:

filter (good . value) = filter (good . value) . filter (ok . value)

Workflow: state it as a RULE, then appeal to a general lemma

(some mucking about)

Mostly a lot of simplification and unfolding. Some practical aspects: getting unfoldings and coercions.

Q: About the proof you showed: not q imples not p of x.... I would have written it p implies q. Is this for a technical reason?

A: No, I happened to type the letters in that order. I probably started writing on the right hand side, and then wrote the left hand side.

Q: Do you have any format for Hermit itself? Semantics?

A: There's not formal logic or semantics. Your ability to demonstrate truth is based on what you can transform. All transforms are assumed to be correct. I would love to dive into that and prove some things are actually valid to use in all cases...

Q: Have you tried to use this script for a proof on a slightly different program, to see how much has to change?

A: The nice thing about universally quantified variables in lemmas is we can prove a general property; this property, we didn't assume it, I proved it. You can generally use it in other cases. You can use these commands in the consequent to apply them to it... the reuse story is better than before. It's all user directed, so you still have to point to a poin in the program. We haven't done a whole bunch of work in taking one transformation and applying to programs; ust concat vanishing transformations. We have one script.... (Did you say we'd be able to write tactics in Haskell?) Hopefully once the ghci basis works, instead of writing into a scripting language to KURE, you should just write KURE combinators directly.

Q: (Gundry) You mentioned a problem with newtype coercions getting in the way. What about reasoning with representational equality, rather than nominal equality.

Consistent use of units is a good idea! Typechecker?

Goal: stop unit errors, and type inference, and make conversions (type classes).

(Demo!)

(beautiful type error.. But at the top, it just says it couldn't match m/s with s)

(exponentiation and derived units work in TH quasiquoter.)

(convert has an unpleasant type)

"Adam, when the demo doesn't work, click here."

Type infrastructure: kind Unit, and then stuff for constructing things. Quantity has phantom type for units.

Problem: equational theory of free abelian groups (Andrew Kennedy's work in F#)

Why not encode these as Richard's units library does? It's all about type inference.

Idea: look for equality constriants of kind unit, normalise them and simplify (free abelian group unification). Some tricky cases with quantification, type families and local given constraints.

Idea: dynamic unification. Instead of looking at constraints and either solving or not, if we can't solve it, leave it alone and come back later.

Q: A lot of people have thought about this in the past. One of the things about ho you're doing it, the syntax looks crap. So do you have a sense if it's a way to have a flexibly plug things in, and have a smooth... Haskell has complex syntax already. Can we have actual natural looking unit syntax? And then corresponding with type errors....

A: Yes, it's certainly true. Quasiquote... good for input, but output leaves room for desired? (I don't even think the input is nice, if you always have to quasiquote.) There's certianly more to be done. An excitin direction this work can take is to make more possible plugins, e.g. to the parser, or something else would be really valuable to make these extensions more modular

Q: We've gotten a good place with reproduceable packaging, even shell scripts... I worry with compiler plugins; how does packaging works? If I have a shell script that depends on a type plugin; pragmas don't have...

A: The short answer is, there is no packaging story. It's a normal Cabal package, versioned in the same way nad depended on the same way. The command line says, just load it in the same way as an import statement. It just works.

Q: These axioms... a finite fixed number of aioms... you have to generate them on the fly?

A: Something that wasn't clear enough earlier... it's not generating proofs at the moment; every ... in principle what you should do, the plugin should be able to specify the collection mechanisms... necessarily be... there's still work to make it easier for plugin writers to define axioms.

Q: Units... promote a data type? Set of data types is fixed?

A talk for solving numeric constraints in Haskell programs

Example: length-indexed vector reverse

What are the generic things a Haskell compiler has to do? This results in a nice integration with SMT. The main point of a Haskell compiler is to get implications.

GHC can do forward reasoning: you can assume facts that are implied by assumptions. Also, unsatisfiable assumptions are unreachable. (Working with assumption.)

Trickiest and most important: constraints you're trying to prove are used for type inference.

BTW: it is always sound to pick whatever you want for unification variables. But if you pick them any old way, you'll just reject programs. The middle says by picking the type we are not losing any generality.

Constraint solver:

Solve goals

Detect unsatisfiable assumptions

Detect unsolvable

Compute derived facts

SMT solvers have decision procedures for lots of things. SMT solver has a state of assumptions; now you can ask if the constraints are consistent, or add more things.

Trouble: what facts should SMT solver compute?

Goal: (5 * a <= 7, 10 * a <= 20). No assumptions.

Try to solve (the negation): it's SAT!

Check for satisfiability (the positive). Result: Sat x = 2.

Check for improvements: UNSAT!

Compute improvement: x = 2.

Solve (5 * 2 >= 7, 10 * 2 <= 20)

Have to find some linear relations between variables. What kind of generalization is a black art. Fortunately generalization is not...

https://github.com/yav/type-nat-solver (GHC plugin)

Q: (Adams) What types of types can I now infer that take advantage of this.

A: Well, the vector reverse is an example.

Q: Do you generate evidence/proof terms?

A: No. In the prototype, it just puts fake evidence; the SMT solver said so. But some produce proof terms; we could potentially translate those to GHC language.

Q: In the example with x = 2; what happens if you find 2 works but it's not unique?

A: No improvement; you keep going. I have a few other things; maybe I need to prove x = y, if they happen to have the same value? Try some generalizations (The improvement is always optional) yes but if you don't do it you won't be able to typecheck

Q: I'd appreciate more examples with improvement. The example required it. How about the last slide; it's not complete? That is to say, I think it requires improvement; what is the improvement that happened in the vector example; what about an example where it is not complete?

A: It is generally hard to show it; but you get unification variables all over the place, but you end up with a lot of constraints; it's a variable, you can't solve it. x + 0 = y, and somewhere else we need to know x = y, then it can't figure it out. (I don't see that it makes things incomplete; x ~ y?) When you really need to do that business, type signature, then you can't just add more constraints. Sometimes it will work without because it just delays constraints.

Q: How performant is doing these roundtrips to the SMT solver?

A: Not super performant... first the way I showed it here is not exactly how it works; a lot of solvers are incremental. There was a lot of duplicatoin; you don't assume all the things all the time, it has a stack based discipline; you assert things, unassert. That overhead is not bad. I've only tried for small examples. The good thing is, it's modular. As long as your function is not huge, the questions you'll ask are very simple. But the implementation communicates over a pipe over text.

Q: How does this compare with LiquidHaskell?