Compile-time invariant/property checking in Elm

Question

I have some value constraints/properties that I want to check at compile-time. In this example, I want to track whether a vector is normalized or not. I think I have a solution, using type tags, but I need someone with some Elm/FP experience to tell me if I have missed something obvious. Thank you.

module TagExperiment exposing (..)

type Vec t = Vec Float Float Float
type Unit = Unit
type General = General

toGeneral : Vec t -> Vec General
toGeneral (Vec x y z) =
    Vec x y z

scaleBy : Vec t -> Vec t -> Vec t
scaleBy (Vec bx by bz) (Vec ax ay az) =
    {- Operate on two General's or two Unit's. If you have one of each,
       then the Unit needs to be cast to a General.
    -}
    let
        mag =
            sqrt ((bx * bx) + (by * by) + (bz * bz))
    in
    Vec (ax * mag) (ay * mag) (az * mag)

-- These cases work as desired.

a : Vec Unit
a = Vec 0 0 1

b : Vec General
b = Vec 2 2 2

d : Vec Unit
d = scaleBy a a

e : Vec General
e = scaleBy b b

g : Vec General
g = scaleBy (toGeneral a) b

h : Vec General
h = scaleBy b (toGeneral a)

-- Here is where I have trouble.

c : Vec t -- unknown... uh-oh
c = Vec 3 3 3

f : Vec t -- still unknown... sure
f = scaleBy c c

i : Vec Unit -- wrong !!!
i = scaleBy a c

j : Vec Unit -- wrong !!!
j = scaleBy c a

k : Vec General -- lucky
k = scaleBy b c

l : Vec General -- lucky
l = scaleBy c b

{- The trouble is that I am not required to specify a tag for c. I guess the
   solution is to write "constructors" and make the built-in Vec constructor
   opaque?
-}

newUnitVec : Float -> Float -> Float -> (Vec Unit)
newUnitVec x y z =
    -- add normalization
    Vec x y z

newVec : Float -> Float -> Float -> (Vec General)    
newVec x y z =
    Vec x y z

user_2014893 · Answer

Yes, without Dependant Types the most ergonomic way to ensure constraints on values at compile time is to use opaque types along with a "Parse" approach.

Perhaps something like:

module Vec exposing (UnitVector, Vector, vectorToUnit)


type UnitVector
    = UnitVector Float Float Float


type Vector
    = Vector Float Float Float


vectorToUnit : Vector -> Maybe UnitVector
vectorToUnit (Vector x y z) =
    case ( x, y, z ) of
        ( 0, 0, 0 ) ->
            Nothing

        _ ->
            normalize x y z

Then, with the only ways to get a UnitVector both defined inside this module and known to obey the constraints, then any time you see a UnitVector at compile-time it is correct to assume the constraints are met.

For vectors in particular, it may be worth having a look at ianmackenzie/elm-geometry for comparison?

Compile-time invariant/property checking in Elm

1 Answers