如何用我的玩具语言正确评估此值

Question

我正在制作一种玩具语言，我希望能够使用相同的构造函数对浮点数和整数进行算术运算，如下所示(下面提供了最小示例)。

data Expr a where
NumberConst :: Number a -> Expr (Number a)
Mul         :: Expr (Number n) -> Expr (Number n) -> Expr (Number n)
data family Number :: * -> *
data instance Number Integer = NumInt Integer deriving (Eq, Ord, Show)
data instance Number Float   = NumFloat Float deriving (Eq, Ord, Show)
class (Eq a, Ord a, Num a) => SquanchyNum a where
toDigit  :: Number a -> a
divide :: Number a -> Number a -> a
mul    :: Number a -> Number a -> a
sub    :: Number a -> Number a -> a
add    :: Number a -> Number a -> a
instance SquanchyNum Integer where
toDigit  (NumInt x)            = x
divide (NumInt x) (NumInt y) = x `div` y
mul    (NumInt x) (NumInt y) = x * y
sub    (NumInt x) (NumInt y) = x - y
add    (NumInt x) (NumInt y) = x + y
instance SquanchyNum Float where
toDigit  (NumFloat x)                = x
divide (NumFloat x) (NumFloat y) = x / y
mul    (NumFloat x) (NumFloat y) = x * y
sub    (NumFloat x) (NumFloat y) = x - y
add    (NumFloat x) (NumFloat y) = x + y

eval :: Expr a -> a
eval (NumberConst a) = a
eval (Mul a b) = (eval a) `mul` (eval b) <-- this line makes the problem visible

在 ghci 中，我收到以下错误

*Main> :r
[2 of 3] Compiling Lib              ( /home/michael/git/brokensquanchy/src/Lib.hs, 
interpreted )
/home/michael/git/brokensquanchy/src/Lib.hs:45:18: error:
• Occurs check: cannot construct the infinite type: n ~ Number n
Expected type: a
Actual type: n
• In the expression: (eval a) `mul` (eval b)
In an equation for ‘eval’: eval (Mul a b) = (eval a) `mul` (eval b)
• Relevant bindings include
b :: Expr (Number n)
(bound at /home/michael/git/brokensquanchy/src/Lib.hs:45:13)
a :: Expr (Number n)
(bound at /home/michael/git/brokensquanchy/src/Lib.hs:45:11)
|
45 | eval (Mul a b) = (eval a) `mul` (eval b)
|                  ^^^^^^^^^^^^^^^^^^^^^^^
Failed, one module loaded.

但是当我在 ghci 中手动尝试以下内容时，它可以工作

(eval (NumberConst (NumInt 6))) `mul` (eval (NumberConst (NumInt 2)))
12

这让我相信我没有在 eval 的类型签名中提供足够的细节。解决方案是什么？

编辑 - 我认为我既没有正确处理这个问题，也没有清楚地解释它。

解决卢基的问题

您已经用a标记了类型-您可以从类型推断出它将是哪个构造函数-构造函数对您没有任何作用。为什么不从这个源文件中消除Number a，只是用无处不在的a替换它？

好的，让我们用NumberConst来做到这一点

data Expr a where
NumberConst :: a -> Expr a

现在我可以这样做了

:t NumberConst ("bad code") 
NumberConst ("bad code") :: Expr [Char]

我不想那样做。

因此，我需要一种方法来(1) 强制我的算术构造函数只能有一个Int或Float(2)避免重复的构造函数，一个用于 Int 和 Float。我应该能够在Int或Float上使用算术构造函数。(3)能够知道是Int还是Float，以便我处理除法。

数据族加类型类是我认为能够实现这一目标的方式。如果没有必要，我完全赞成更简单的方法。我只是不知道那是什么。

Answer 1

好的，让我们用 NumberConst 来做这件事

data Expr a where
NumberConst :: a -> Expr a

现在我可以这样做

:t NumberConst ("bad code")
NumberConst ("bad code") :: Expr [Char]

我不想那样做。

明白了。在这里，我们遇到了一个哲学问题：强类型的意义何在？许多程序员会说，拒绝格式错误的程序。这当然是一个优势，但Haskell长期以来一直遵循西蒙·佩顿·琼斯(Simon Peyton Jones)所说的性感类型的方向：类型签名不应该只是禁止事情，而是引导你，以便程序自动正确。

换句话说，仅仅为了防止NumberConst "bad code"而限制NumberConst中的类型是不性感的。相反，您应该只需要实际需要的属性。这不需要任何数据系列，只需要一个类型类。似乎你基本上只需要Num/Fractional，除了一个除法，对于积分和/对于浮动类型，它兼作div。(顺便说一句，这可能不是一个好主意，但让我们继续吧。

class Num a => Divisible a where
divide :: a -> a -> a
instance Divisible Int where divide = div
instance Divisible Float where divide = (/)
data Expr a where
NumberConst :: Divisible a => a -> Expr a
Mul         :: Expr n -> Expr n -> Expr n

这个约束足以证明每一个非无限Expr a都满足Divisible a。当你实施eval你会发现GHC拒绝承认这一点。作为解决方案，您可以简单地将约束也添加到Mul

Mul         :: Divisible n => Expr n -> Expr n -> Expr n

。严格来说，这是多余的，但这可能无关紧要;或者，您可以以延续传递样式实现一个帮助程序函数，该函数从表达式中提取证明：

{-# LANGUAGE RankNTypes #-}
evalCPS :: Expr a -> (Divisible a => a -> r) -> r
evalCPS (NumberConst n) q = q n
evalCPS (Mul x y) q = x `evalCPS` x' -> q $ x' * eval y
eval :: Expr a -> a
eval = evalCPS id

---

(3)能够知道是Int还是Float，以便我处理除法。

上述解决方案不会这样做。事实上，任何人都可以在以后添加更多实例。如果你不想这样，如果你真的想只允许Int和Float，并希望能够找出它是哪一个，那么我建议你使用单独的构造函数，但仅限于常量：

data Expr a where
IntConst :: Int -> Expr Int
FloatConst :: Float -> Expr Float
Mul :: Expr a -> Expr a -> Expr a

现在，您可以再次使用 CPS 版本的eval，它允许不同的延续，具体取决于它是Int还是Float：

evalCPSMono :: Expr a -> (Int -> r) -> (Float -> r) -> r
evalCPSMono (IntConst i) qI _ = qI i
evalCPSMono (FloatConst w) _ qF = qF w
evalCPSMono (Mul x y) qI qF
= evalCPSMono x (x' -> qI $ x' * eval y)
(x' -> qF $ x' * eval y)

或者，您可以将限制表示为具有封闭类型族的两种类型。

type NumberAllower a where
NumberAllower Int = Int
NumberAllower Float = Float
NumberAllower a = Void
data Expr a where
NumberConst :: NumberAllower a -> Expr a
...

这可以防止任何人编写NumberConst "bad code"。但它不做的是让您找出Expr中包含的特定类型。无论如何，您最终都必须从外部手动要求它。不性感。

仍然只有一个NumberConst构造函数的替代方法，但确实可以让您获得确切的类型，如下所示(这可能是您最初尝试编写的内容)：

data Number a where
It'sInt :: Int -> Number Int
It'sFloat :: Float -> Number Float
data Expr a where
NumberConst :: Number a -> Expr a
Mul :: Expr a -> Expr a -> Expr a

这是在实践中