(WIP) Elm-Refine: Proving an Elm expression has the inferred type

[Lucas_Payr]

This is a follow up to a post I did a year ago:

Elm-Refine: Proposal

Greetings everyone, I’m currently studying computer mathematics at the University of Linz/Austria and am now working on my master-thesis: Refinement types for Elm. In this post I will first explain the main concept and then propose a syntax. I would be grateful if you could give me feedback regarding the syntax. What are Refinement Types? Let’s look at the following example. {-| @refine \int -> int /= 0 -} type alias IntWithoutZero = Int dividedBy : IntWithoutZero -> Int -> Int dividedBy…

In this post I’ll give an overview of that has happened in the last year.

For a quick recap what refinement types are, checkout the slides of the presentation I did at the Elm Vienna Meetup.

My thesis has three parts:

1.) Proving an Elm expression has the inferred type.
2.) Proving that adding Refinement types will not break anything.
3.) Implement a type checker for refinement types (as a fork of Elm-Analyse)

It took me this entire year to finish the first part, so this post will be about that.

---

What “is” an Elm Expression?

The first thing I needed to do, was to specify what I mean by an “Elm Expression”. Are we talking about 1.18 or 1.19? What about Runtime errors: should an Elm expression that causes a Runtime error be considered a “valid” Elm Expression? So I started by writing my own formal language. (A formal language is more abstract than a programming language: It only exists on paper) I added most features of 1.19, but also excluded some:

• No White space sensitivity
• No Pattern matching (I dropped it midway, as it would have cost a lot of additional time)
• No Phantom Types, Extendable Records, Never Type and Opaque Types
• No Recursion (To avoid Runtime errors. Instead, I added foldl as a build-in primitive)
• No TEA
• No Ports

Here are the syntax and the semantics of my formal language.

You can think of the syntax as a big custom type describing the language structure. We actually have a lot of interlinked custom types, most importantly: a Value type and a Program type. The Semantics is a function that gives the syntax a meaning: For a given Program the semantics can compute the resulting Value.

For more on this, checkout Richard Feldman’s tak.

Richard Feldman - Keynote - Elm Europe 2019

What is Elm’s Type system?

You might know that Elm’s type system is very special. An expression may have different types. For example the expression [] may have the type List a or List Int or List (List a) and so on. The technical term is Polymorphic Type System. (Poly = Multiple, Morph = form)
You might also know that Elm is in the ML Language family and thus has the same underlying type system: The Hindley-Milner Type System.

So, here is my definition of the Hindley-Milner Type System.

Once this was defined, I introduced inferene rules: Rules that lets me infer the type of an expression.

Proving an Elm expression has the inferred type.

What is left to do, is to prove that for any Elm expression, the resulting value of the semantics matches the inferred type.
The proof is fairly easy: I have a function values : Type -> Set Value that returns all values of a type. I then start by pattern matching my way though the syntax (a costum type). For each case I take the inferred type type and the resulting value value of the semantic and check values type |> Set.contains value. If for every case the result is True then I have proven that the result of any Elm expression has the inferred type.

Here is the mathematical proof.

Example

I actually have implemented all the above in a research tool called K Framework.

Here is a quick walkthrough of the implementation with a small example at the end. (Example starts on page 4)

What’s next?

Next year I expect to add Refinement types to the formal language (and again prove that this does not break anything) and finally to start the implementation of the type checker.