haskell - 我可以在 Haskell 中定义参数不相等的参数数据类型吗？

Question

问题：

假设我们有一个乘客，其起点和终点分别表示为：

data Passenger a = Passenger { start :: a
                               , end :: a
                             }

问题：

如何将类约束应用于起点不应等于终点的乘客？

PS： 我在 Scala 社区问过类似的问题，但没有得到任何答案。考虑到scala 的精炼库是受Haskell 精炼的启发，也听说过液体 Haskell，我想知道如何使用 Haskell 解决它？

标签： haskelltypestype-systemsrefinement-typeliquid-haskell

Answer 1

我刚看到这个。您可以通过在字段上指定细化来做到这一点end，例如：

{-@ data Passenger a = Passenger 
      { start :: a
      , end   :: {v:a | v /= start} 
      } 
  @-}

data Passenger a = Passenger 
  { start :: a
  , end   :: a
  }                        

ok :: Passenger String 
ok = Passenger "Alice" "Jones"

bad :: Passenger String
bad = Passenger "Bora" "Bora"

你可以在这里在线玩这个：

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1551137259_16583.hs