haskell - Haskell 中的隐式静态类型转换(强制)

Question

问题

考虑 Haskell 中的以下设计问题。我有一个简单的符号 EDSL，我想在其中表达变量和一般表达式(多元多项式)，例如 x^2 * y + 2*z + 1 .另外，我想用表达式表达某些符号方程，比如x^2 + 1 = 1 ，以及定义，如 x := 2*y - 2 .

目标是:

变量和通用表达式有一个单独的类型 - 某些
函数可能适用于变量而不是复杂的表达式。
例如，定义运算符 :=可能是类型(:=) :: Variable -> Expression -> Definition它不应该
可以将复杂表达式作为其左侧传递
参数(尽管应该可以将变量作为其
右侧参数，没有显式转换 )。

让表达式成为 Num 的实例, 这样就可以
将整数文字提升为表达式并使用方便的
常见代数运算的符号，如加法或
不引入一些辅助包装运算符的乘法。

换句话说，我希望对表达式进行隐式和静态类型转换(强制)。现在，我知道 Haskell 中没有隐式类型转换。尽管如此，某些面向对象的编程概念(在这种情况下为简单继承)在 Haskell 的类型系统中是可以表达的，无论有没有语言扩展。如何在保持轻量级语法的同时满足上述两点？甚至可能吗？

讨论

很明显这里的主要问题是 Num的类型限制，例如
(+) :: Num a => a -> a -> a
原则上，可以为变量和表达式编写单个(广义)代数数据类型。然后，可以写 :=以这种方式，左侧表达式被区分并且只接受变量构造函数，否则会出现运行时错误。然而，这不是一个干净的静态(即编译时)解决方案......

例子

理想情况下，我想实现轻量级语法，例如

computation = do
  x <- variable
  t <- variable

  t |:=| x^2 - 1
  solve (t |==| 0)

特别是，我想禁止像 t + 1 |:=| x^2 - 1自从 :=应该给出一个变量的定义，而不是一个完整的左侧表达式。

Answer 1

要利用多态性而不是子类型化(因为这就是 Haskell 中的全部内容)，不要认为“变量就是表达式”，而是“变量和表达式都有一些共同的操作”。这些操作可以放在一个类型类中:

class HasVar e where fromVar :: Variable -> e

instance HasVar Variable where fromVar = id
instance HasVar Expression where ...

然后，而不是类型转换事物，使事物具有多态性。如果您有 v :: forall e. HasVar e => e ，它既可以用作表达式，也可以用作变量。

example :: (forall e. HasVar e => e) -> Definition
example v = (v := v)  -- v can be used as both Variable and Expression

 where

  (:=) :: Variable -> Expression -> Definition

骨架使下面的代码类型检查: https://gist.github.com/Lysxia/da30abac357deb7981412f1faf0d2103

computation :: Solver ()
computation = do
  V x <- variable
  V t <- variable
  t |:=| x^2 - 1
  solve (t |==| 0)