如何进行重构,使得得分高于特定数量的分数是无法代表的？

Question

如何进行重构,使得得分高于特定数量的分数是无法代表的？

例如,如何使用以下代码并使编译器拒绝任何超过总分为11分的镜头？

let results = (player1, player2) |> makeFieldBasket TwoPointer
                                 |> makeFoulShots   ThreeFoulShots
                                 |> makeFieldBasket TwoPointer
                                 |> makeFoulShots   TwoFoulShots
                                 |> makeFieldBasket TwoPointer

上面代码的输出如下:

 val results : FoulShooter * FieldShooter =
  (FoulShooter {Score = 11;}, FieldShooter {Score = 0;})

现在我想构建我的代码,以便无法编译额外的镜头.

例如,我希望编译器拒绝超过11分的额外犯规:

let results = (player1, player2) |> makeFieldBasket TwoPointer
                                 |> makeFoulShots   ThreeFoulShots
                                 |> makeFieldBasket TwoPointer
                                 |> makeFoulShots   TwoFoulShots
                                 |> makeFieldBasket TwoPointer
                                 |> makeFoulShots   FoulShot

目前,上述代码是合法的.

整个代码如下:

(*Types*)
type Player = { Score:int }

type FieldShot = TwoPointer| ThreePointer
type FoulShots = FoulShot  | TwoFoulShots | ThreeFoulShots

type FoulShooter  = FoulShooter  of Player
type FieldShooter = FieldShooter of Player

(*Functions*)
let shoot lastShot player =
    (player.Score + lastShot)

let fieldShot (fieldShooter, shot) =

    let player = match fieldShooter with
                 | FieldShooter player -> player

    match player.Score with
    | score when score >= 11 -> score
    | _ ->  match (fieldShooter, shot) with
            | FieldShooter player, shot -> match shot with
                                           | TwoPointer   -> player |> shoot 2
                                           | ThreePointer -> player |> shoot 3

let foulShot (foulShooter, shot) =

    let player = match foulShooter with
                 | FoulShooter player -> player

    match player.Score with
    | score when score >= 11 -> score
    | _ ->  match (foulShooter, shot) with
            | FoulShooter player, shot -> match shot with
                                          | FoulShot       -> player |> shoot 1
                                          | TwoFoulShots   -> player |> shoot 2
                                          | ThreeFoulShots -> player |> shoot 3

let makeFoulShots foulShots (shooter, defender) = 
    FieldShooter { Score= foulShot (shooter, foulShots) }, defender

let makeFieldBasket fieldBasket (shooter, defender) =
    FoulShooter { Score= fieldShot (shooter, fieldBasket) }, defender

let turnover (shooter, defender) = (defender, shooter)

(*Client*)
let player1, player2 = FieldShooter { Score=0 } ,
                       FieldShooter { Score=0 }

let results = (player1, player2) |> makeFieldBasket TwoPointer
                                 |> makeFoulShots   ThreeFoulShots
                                 |> makeFieldBasket TwoPointer
                                 |> makeFoulShots   TwoFoulShots
                                 |> makeFieldBasket TwoPointer
                                 |> makeFoulShots   FoulShot

Answer 1

您希望的功能(并且您不是唯一的功能!)称为依赖类型(维基百科,以及快速介绍).更确切地说,您的特定示例将被称为细化类型,因为在这种情况下,类型Score对值的依赖性n由谓词表示n <= 11.

支持依赖类型并非易事.它要求编译器运行完整的定理证明程序,以便正确检查代码中所有可能的执行路径,并确保不,带'a -> Integer<11>签名的此函数永远不会返回大于11的输出.

依赖类型目前尚未在主流编程语言中实现,例如F#,Haskell,Erlang或Clojure.但是,它们是用一些学术和/或研究语言实现的,通常是在数学语境中; 上面的维基百科文章可能有完整的列表.

如果您需要对依赖类型进行认真的工作,Coq是其中最成熟和最完善的,而Agda可能是下一个并且更加现代化.

否则,如果你只是在处理一个个人项目,你可能想要查看F*,这是一个依赖类型的语言,它是基于F#并且编译为F#的活动开发,应该是最简单的语言.你去接.

现在,假设我们将在当前十年左右坚持"仅"F#,您问题的传统解决方案是将可能无效的值存储在受歧视的联合中.

带有自定义+运算符的简单DU 可以防止您意外添加无效分数:

type Score = InvalidScore | ValidScore of int<pts>

let (+) s1 s2 = match (s1, s2) with
   | ValidScore a, ValidScore b when (a + b) <= 11<pts> -> ValidScore (a + b)
   | _ -> InvalidScore

如果您还想阻止自己首先创建无效分数,那么我们需要一个基于访问者修饰符的稍微复杂的实现.

也就是说,我们可以将整个事物放入一个模块中,将DU的两个子类private放到该模块中,并且只暴露安全的方法/属性,如下所示:

[<AutoOpen>]
module Score = 

    type Score = private InvalidScore | ValidScore of int<pts> with
       static member Create n = 
          if n > 11<pts> then InvalidScore else ValidScore n
       member this.GetPoints = 
          match this with 
          | InvalidScore -> None 
          | ValidScore x -> Some x

    let (+) s1 s2 = 
       match (s1, s2) with
       | ValidScore a, ValidScore b when (a + b) <= 11<pts> -> ValidScore (a + b)
       | _ -> InvalidScore


let x = ValidScore 12<pts> // won't compile

let y = Score.Create 12<pts> // compiles, but if you call y.GetPoints you get None