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

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课程开始研究这个tic-tac-toe API,这需要做以下事情:

takeBack:选择一个完成的棋盘或一个至少有一次移动的棋盘,然后返回一个棋盘.在空板上调用此函数是编译时类型错误.

我认为可以做一些非常花哨的类型级编程.但即便如此,我也不认为刚刚参加了为期两天的函数式编程介绍的人可以知道它.还是我错过了什么？

更新

基于@ user2407038给出的示例和来自@Cirdec的说明,我写了这个,当你尝试takeBack在一个很棒的空板上时,它会产生编译时错误.

然而 - 稍微移动球门柱 - 这个技巧似乎有限.还有一个要求是你不能继续已经结束的游戏.

移动:采取一个井字板和位置并移动到该位置(如果没有占用)返回一块新板.此功能只能在空白或正在播放的电路板上调用.调用已完成的游戏板上的移动是编译时类型错误.

看起来似乎不是一个简单的技巧,可以在复杂逻辑的情况下使用移动,以确定游戏是否结束.

{-# 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是为了方便,但不需要它.