是否有可能为同一个构造函数有不同的行为？

Question

我正在写一个SQL解释器.我需要在编译时区分不正确的表达式和运行时错误.

我会给你一个应该是格式良好的例子,但可能在运行时失败.

SELECT $ [ColumnName "first_name" `AS` "name"] `FROM` TABLE "people.csv" `WHERE` (ColumnName "age" `Gte` LiteralInt 40)

我想专注于表达:

(ColumnName "age" `Gte` LiteralInt 40)

这应该通过类型检查器.但是,说"年龄"并不包含可以表达为a的东西LiteralInt.

所以我想要Gte产生类似的东西IO Bool(暂不考虑异常处理).

但我并不总是需要Gte制作一个IO Bool.如果我有这样的事情:

(LiteralInt 40 `Gte` LiteralInt 10)我只需要一个Bool.或类似的东西: (LiteralInt 40 `Gte` LiteralBool True)需要在编译时失败.

所以,我一直在玩弄数据系列和GADT,并且已经落下了许多死胡同,如果我解释它们就会混淆这种情况.

我的问题是否有意义,如果是这样,我可以通过一个探索的途径来解决问题？

Answer 1

所以我想要Gte产生类似的东西IO Bool(暂不考虑异常处理).

但我并不总是需要Gte制作一个IO Bool.

这是不可能的(也不是可取的).Gte必须始终返回相同的类型.此外,您可能希望将查询的构造与其执行分开...

或类似的东西:(LiteralInt 40 `Gte` LiteralBool True)需要在编译时失败.

现在这更合理了.如果您决定沿着这条路走下去,您甚至可以使用新TypeError功能自定义GHC报告的类型错误.但是,坚持一个简单的例子只涉及到LiteralInt,LiteralBool并且Gte,您可以使用GADT执行类似下面的操作:

{-# LANGUAGE GADTs #-}

data Expr a where
  LiteralInt :: Int -> Expr Int
  LiteralBool :: Bool -> Expr Bool
  Gte :: Expr Int -> Expr Int -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  ColumnName :: String -> Expr a

然后,以下将全部编译:

ColumnName "age" `Gte` LiteralInt 40
LiteralInt 40 `Gte` LiteralInt 10
(LiteralInt 40 `Add` ColumnName "age") `Gte` LiteralInt 10

而以下不会:

LiteralInt 40 `Gte` LiteralBool True
LiteralInt 40 `Add` LiteralBool True

但是,说"年龄"并不包含可以表达为a的东西LiteralInt.

你可能会潜在地使这也是编译时,如果你知道你在编译时的架构和你想要做很多类型两轮牛车的.更简单的解决方案就是在执行查询时进行错误处理.所以你会看到类似的功能

evalExpr :: Expr a -> ExceptT e IO a

你可能会在这里对列的类型进行适当的检查.