haskell - 具有单个构造函数的 GADT

Question

这是一个示例代码:

{-# LANGUAGE GADTs #-}

data NumGadt a where
  NumGadt :: Num a => a -> Int -> String -> Bool -> NumGadt a

getNum :: NumGadt a -> a
getNum (NumGadt a _ _ _) = a

现在假设我想写一个这样的函数:

successor :: NumGadt a -> a
successor x = 1 + getNum x

问题是这不会编译，错误是关于 No instance for (Num a)
一个可能的解决方案是

successor :: NumGadt a -> a
successor x@(NumGadt _ _ _ _) = 1 + getNum x

但这相当丑陋，在更多地方使用它会变得非常丑陋。

所以问题是，有没有办法让编译器意识到这种类型只有一个构造函数，并从中推断出约束？

Answer 1

你可以定义一个 withNum带来 Num a 的 helper 范围内的字典。

{-# LANGUAGE GADTs, RankNTypes #-}

data NumGadt a where
  NumGadt :: Num a => a -> Int -> String -> Bool -> NumGadt a

withNum :: NumGadt a -> (Num a => b) -> b
withNum (NumGadt _ _ _ _) y = y

getNum :: NumGadt a -> a
getNum (NumGadt a _ _ _) = a

successor :: NumGadt a -> a
successor x = withNum x (1 + getNum x)

在我看来，这并不比匹配 successor 中的构造函数好多少。 ，即使名称 withNum更自我记录。

请注意，您甚至可以使用较短的记录语法:

successor :: NumGadt a -> a
successor x@NumGadt{} = 1 + getNum x