Monday, December 3, 2018

Blodwen & Agda

A couple of interesting tweets came out over the weekend, referring to new resources on the web.

Blodwen

The first is a Code Mesh talk given by Edwin Brady on Blodwen, a.k.a., Idris 2. Among Blodwen's more interesting capabilities: improved program inference, and linear types. These interact in a fascinating way: using program inference to implement the function

	transform : Vect m (Vect n A) -> Vect n (Vect m A)

“succeeds” in writing type-correct, but semantically incorrect code. Adding a one-use constraint in blodwen inferring code which is both type- and semantics-correct.

Programming Language Foundations in Agda

The second is the publication of the web-based textbook Programming Language Foundations in Agda by Philip Wadler and Wen Kokke.

at

No comments:

Post a Comment

Subscribe to: Post Comments (Atom)

12/4/18: The Path Forward

We took a quick look today at the Nat-Nat problems , and in particular around the distinction between + and plus . But the main conversatio...

  • Our First Meeting
    At our first meeting, we agreed to read “The Little Typer” through Chapter 4 (but read below), and seriously outgrew our space, with twe...
  • 12/4/18: The Path Forward
    We took a quick look today at the Nat-Nat problems , and in particular around the distinction between + and plus . But the main conversatio...
  • Nat-Nat Problems
    Problem 1 . Write the functions max and monus , where (claim max (-> Nat Nat Nat)) is the usual max function, e.g., ...