haskell - (一个简单的方法)使调用具有特定值的函数是编译时错误？

Question

我认为不可能(或需要某些语言扩展)来创建这样的函数

f :: Maybe Int
f (Just n) = n
f Nothing = ... -- a compile-time error

你也无法创建这样的函数:

g :: MyClass a => Int -> a
g n | n < 10    = TypeClassInstance
    | otherwise = OtherTypeClassInstance

所以，我正在研究著名的 NICTA FP course 的井字游戏 API。那is required to do things like :

takeBack: takes either a finished board or a board in-play that has had at least one move and returns a board in-play. It is a compile-time type error to call this function on an empty board.

我认为可以进行一些非常奇特的类型级编程。但即使是这样，我认为刚刚学习了 2 天函数式编程入门的人也不会知道这一点。还是我错过了什么？

更新

基于@user2407038给出的示例和@Cirdec的澄清，我写了这个，当你尝试在空板上takeBack时，它确实会产生编译时错误，这很棒。

然而——稍微移动一下球门柱——这个技巧似乎有局限性。还有一个要求是你不能在已经结束的游戏中继续前进。

move: takes a tic-tac-toe board and position and moves to that position (if not occupied) returning a new board. This function can only be called on a board that is empty or in-play. Calling move on a game board that is finished is a compile-time type error.

在逻辑复杂的情况下，用类型计数走步来判断游戏是否结束似乎不是一个简单的技巧。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data N = S N | Z

data Stat
  = Empty
  | InPlay
  | Won
  deriving Show

data Board (n :: N)
  = Board Stat [Int]
  deriving Show

newBoard :: Board Z
newBoard = Board Empty []

move :: Int -> Board a -> Board (S a)
move x (Board Empty []) = Board InPlay [x]
move x (Board InPlay xs) = Board Won (x:xs)

takeBack :: Board (S a) -> Board a
takeBack (Board InPlay [x]) = Board Empty []
takeBack (Board InPlay (x:xs)) = Board InPlay xs
takeBack (Board Won (x:xs)) = Board InPlay xs

main :: IO ()
main = do
  let
    brd = newBoard    -- Empty
    m1 = move 1 brd   -- InPlay
    m2 = move 2 m1    -- Won
    m3 = move 3 m2    -- Can't make this a compile-time error with this trick
    tb2 = takeBack m2 -- Won
    tb1 = takeBack tb2 -- InPlay
    tb0 = takeBack tb1 -- Empty -> Compile-time error Yay!
  return ()

Answer 1

您可以使用 GADT(广义代数数据类型)执行类似于第一个示例的操作；

data SMaybe (a :: Maybe *) where 
  SJust :: a -> SMaybe (Just a)
  SNothing :: SMaybe Nothing 

f :: SMaybe (Just a) -> a 
f (SJust a) = a 
-- f SNothing = undefined -- Including this case is a compile time error

虽然我怀疑这有多大用处。解决板问题的最简单的解决方案可能是在您的 Board 数据类型上使用幻像类型参数:

type Empty = False
type NonEmpty = True
data Board (b :: Bool) = Board ...

newBoard :: Board Empty
newBoard = Board ...

setAt :: (Int, Int) -> Bool -> Board a -> Board NonEmpty 
setAt p b (Board ...) = ...

takeBack :: Board NonEmpty -> Board NonEmpty
takeBack (Board ...) = ...

如果您愿意，您可以增加类型级别上存储的信息量。例如，您可以获取填充的“单元格”数量:

data N = S N | Z -- The naturals

data Board (n :: N) = Board ...

newBoard :: Board Z
newBoard = Board ...

setAt :: (Int, Int) -> Bool -> Board a -> Board (S a)
setAt = ...

takeBack :: Board (S n) -> Board (S n)
takeBack = ...

上面的示例使用 DataKinds 是为了方便，但这不是必需的。