Elm中的编译时不变/属性检查

问题描述

我有一些要在编译时检查的值约束/属性。在此示例中,我想跟踪向量是否已归一化。我认为我有使用类型标签解决方案,但是我需要具有Elm / FP经验的人告诉我是否错过了明显的事情。谢谢。

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
    

解决方法

是的,没有依赖类型,在编译时确保对值的约束的最符合人体工程学的方法是使用不透明类型以及“解析”方法。

也许是这样的:

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 ) ->
            Nothing

        _ ->
            normalize x y z

然后,通过的方式来获取在模块内定义的UnitVector并遵守约束条件,那么每次您在编译时看到UnitVector时,是时候假设满足约束条件了。


特别是对于向量,可能值得看看ianmackenzie/elm-geometry进行比较?