Elm-Refine: Proposal

Request Feedback
1

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 a b = b // a

3 |> dividedBy 0 will normally return 0, but using my type-checker it will now throw an error instead:

dividedBy expected the first element to be an IntWithoutZero
but was given an Int instead.

Hint:
I can't convert 0 to IntWithoutZero because 0 /= 0 is false.

These kinds of types are called refinement types. Liquid types are refinement types, where the refinement (int /= 0) can only contain logical operators (not, and, or), constants (like 0), comparisons (<=,<,=, /=) and +. Also it only works for Bool and Int.

Such a type-checker does already exist for Haskell(LiquidHaskell) but its not very beginner friendly. The goal of my thesis would therefore be to make refinement type accessible with a smaller border of entry.

Expected result

Liquid types are still not perfect but I am expecting at least to be able to successfully check the IntWithoutZero type from the example above.

I am also not expecting to have as many features as LiquidHaskell does, mainly because I would rather like to focus on good error messages.

The main work of this thesis will be about the mathematics behind the types and not so much the actual implementation.

Syntax

LiquidHaskell writes its types in a comment block before the normal specification. A similar syntax would look like this:

{-| Checks if the list contains a specific element -}
{- contains : a:Int -> List {b:Int | b >= 0} -> {out:Bool | a >= 0 || not out} -}
contains : Int -> List Int -> Bool
contains =
    List.contains

This is the same syntax as proposed in the original paper, but I feel this might be quite hard to read. Also, this syntax does not go well with both the elm-docs and elm-format.

So instead, I would propose something like

{-| @refine \a -> a >= 0
-}
type alias Nat =
    Int

{-| Checks if the list contains a specific element
@refine \a _ out -> a >= 0 || not out
-}
contains : Int -> List Nat -> Bool
contains x list =
    ..

By using alias types, someone not familiar with my type-checker can still understand what it does.

So I’m interesting to know:

  • Does the proposed syntax look appealing to you?
  • Do you have a better idea how to design the syntax around elm-format and elm-docs?

Edit:
Added \ to the examples. Thanks @Zimm_i48 for that.

14 Likes
2

That’s a super great thesis topic ! I’m not super familiar with it, but I have toyed with ada and I especially like the range syntax:

type Page_Num is range 1 … 2_000;
type Volt is delta 0.125 range 0.0 … 255.0;

3 Likes
3

Yep, coming from the Eiffel world Elm has basically no options to restrict types except by making them opaque. Which is a lot of code to write, and there’s no compile time validation.

But I absolutely hate code in comments. Please don’t go there. This is a big thing in PHP, and we’re getting to the stage we have more code in comments than in code. So please have some kind of invariant for run-time checks if you want to go there. Else the Ada specification if you’re just interested in numbers.

So we get:

constrained type Nat = Int
invariant \a -> a >= 0

I don’t feel type alias is the right thing, it’s not an alias anymore.

8 Likes
4

I’d like to second keeping code out of comments. Would it be possible to add refinements to both functions and types? Something like

@refine \a -> a >= 0
type alias Nat =
    Int

@refine \a :: b :: _ -> a < b 
type alias OrderedList a =
    List a

@refine \a b -> a :: b
insert : a -> OrderedList a -> OrderedList a
insert a b =
    ...

Not sure at all about the syntax for the refinement itself, but something that can be shared across types and functions without having to make the syntax too complicated.

1 Like
5

Correct me if I’m wrong, but aren’t Eiffel and Ada doing their checks in run time? What I am talking about will be in compile time.

Doing this sort of checks in compile time is very experimental.
Multiplication is a nightmare for computers to reason about.
That’s why I feel that using comments is the right way to go. This way people understand that it’s not perfect. This is nothing you would use in production.

6

Yes. But what are maybe a far bigger problem, are Lists. LiquidHaskell can only reason about an element in regard to its following element.
So it would look like this:

{-| @refine \a b -> a < b -}
type alias OrderedList a =
    List a

I really don’t like that, it feels very unintuitive. (:man_shrugging: But I don’t know a better solution)

Another design decision I need to make is whether to allow specific function. Like (::) or List.length. Personally I would love it, but then I don’t know where to stop. Should modBy be allowed? What about getters for records? Or setter? For now, I trend towards not allowing any special function.

7

For now :slight_smile: But in practice that works very well. You catch a lot of bugs that way. But we have more and more CPU cycles to spare, so who knows.

8

I guess the main point of putting this stuff in comments is that your Elm-Refine program is still an Elm vanilla program, that you can publish as an Elm package, etc., as I don’t expect liquid types to make it to the official Elm compiler (at least for a while).

Since you’re asking for comments about the syntax, let me suggest that you do not use arrows in the way you do. Arrows in Haskell’s liquid type syntax do make sense because they correspond to function types (concretely, this becomes a dependent arrow because the types to the right of the arrow can depend on the variable of the type to the left of the arrow). Since you feel that this is too hard to read and want to do it differently, do not reuse the arrow with a new meaning. Here are concrete alternative proposals (but this could really be anything).

  • Still using an arrow but with the normal meaning:

    {-| Checks if the list contains a specific element
@refine contains : x -> _ -> out
@with x >= 0 || not out
-}
contains : Int -> List Nat -> Bool
contains x list =
    ..

  • trying to be closer to the function definition syntax instead:

    {-| Checks if the list contains a specific element
@refine contains x _ = out
@with x >= 0 || not out
-}
contains : Int -> List Nat -> Bool
contains x list =
    ..
1 Like
9

Good Point! :point_up::+1:

I was thinking of the arrow being the arrow of a lambda function (as the refinement is actually just a function)

{-| @refine \a _ out -> a >= 0 || not out-}
contains : Int -> List Nat -> Bool
contains x list =

(I’ve added the \ to the top post as well)

But I do like your succession as well.

10

Ah OK, that makes sense indeed.

11

I’m not knowledgeable in this topic, but along the lines of “can we don’t do this in comments” — can’t refinement functions be just Elm functions?

Pick a naming convention (oops?) say refine*

refineIntWithoutZero int =
        int /= 0

Since these functions aren’t actually “used”, function-level dead code elimination will kick in anyways.

—

Update: Go uses *_test.go for test code to reside and Test* prefix for function names to identify which are test functions. I’d definitely prefer some naming conventions allowing me to “just write Elm” than code in comments.

12

You mean something like

refineOnly42 : Int -> Bool
refineOnly42 num =
    num == 42

is42 : Int -> Maybe Only42
is42 num =
    if num == 42 then
        Just num
    else
        Nothing

{-| This would still be needed to be valid elm code
-}
type alias Only42 =
    Int

Yes, that would work. Personally I don’t like it though, it mixes compile time stuff with runtime stuff. As for your Go example, there both is in runtime and Test* is actually just a normal function, whereas for my refinements the syntax is important. Similar functions might not work, like

refineNotValid =
    (==) 42

refineAlsoNotValid num =
    case num of
        42 -> True
        _ -> False
13

I made an attempt by creating a module that handles RangedInt which is an integer within a range.

type RangedInt
= RangedInt PayLoad

type alias PayLoad =
{ min : Int
, max : Int
, value : Int
}

When, for example, two RangedInt are added, a new RangedInt is created where the min and max are the sum of the ranges.

I used a Decoder to create RangedInt so only run-time checks.

decoder : Int -> Int -> Decoder.Decoder RangedInt
decoder min max =
    Decoder.int |> Decoder.andThen (helper min max)

helper : Int -> Int -> Int -> Decoder.Decoder RangedInt
helper min max value =
    if min > value || max < value then
        Decoder.fail <| outOfRangeErrorMessage min max value
    else
        Decoder.map (construct min max) Decoder.int
14

That’s what fully dependently-typed languages (such as Coq or Agda) do, though. Obviously the consequence is that arbitrary computation can happen at compile time.

15

I don’t want to be “that” guy, but dependent types are more general than refinement types. Generally they look and feel and act the same, but they are different.

My definition of “refinement types” are dependent types that have NO quantifiers (forall, exists) and can be compiled without human intervention (without a proof assistant). Other people use other definitions.

So refinement types would still have a relative fast compile time.

1 Like
16

This looks like an extension proposal for the Elm type system, so I think the best way would be to make it consistent with the rest of the type syntax. Something like:

type alias IntWithoutZero =
    refine Int \int -> int /= 0 

…

It’s better if the comments stay comments.

2 Likes
17

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.