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

我在写一个SQL解释器。我需要在编译时区分格式不正确的表达式和运行时错误。是否有可能对同一构造函数有不同的行为？

我给你一个应该是良构的东西的例子，但可能在运行时失败。

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

我想聚焦于表达：

(ColumnName "age" `Gte` LiteralInt 40)

这应该通过类型检查。但是，说“年龄”并不包含可以表示为LiteralInt的内容。

所以我想Gte产生像IO Bool（目前不在意异常处理）。

但我并不总是需要Gte才能生成IO Bool。如果我有这样的事情：

(LiteralInt 40 `Gte` LiteralInt 10)我只需要一个布尔。或类似的东西： (LiteralInt 40 `Gte` LiteralBool True)需要在编译时失败。因此，我一直在与数据家族和GADT一起玩耍，并且走了很多死路，如果我解释它们，这些死路都会混淆局面。

我的问题是否有意义，如果有的话，是否有我可以遍历的探索路径，这将导致解决方案？

来源

2016-11-18 Michael Litchard

通过让一些表达式返回'Bool'而不是'IO Bool'，你会获得什么？ – chepner

类型安全的SQL接口？在[_The Power of Pi_]中有一个例子（https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf），以及[singletons'文件]中的Haskell翻译（http：//cs.brynmawr埃杜/〜RAE /纸/ 2012 /单身/ paper.pdf）。最大的想法是预先声明模式，并在打开数据库连接时检查它是否与实际模式匹配。 –

谢谢本杰明，我要去兔子洞。 :) –

所以我想Gte产生类似IO Bool（不介意异常处理现在）。

但我并不总是需要Gte才能生成IO Bool。

这是不可能的（也确实不可取）。 Gte将不得不始终返回相同的类型。此外，你可能想分开你的查询的执行与其执行...

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

现在即更合理。如果你决定走这条路，你甚至可以自定义GHC报告的新型TypeError功能的类型错误。然而，坚持涉及刚刚LiteralInt，LiteralBool和Gte一个简单的例子，你可以不喜欢只用GADTs如下：

{-# 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

但是，说“年龄“不包含可以表示为LiteralInt的内容。

您可以可能使这也是编译时，如果你知道你在编译时的架构和你想要做很多类型两轮牛车的。更简单的解决方案就是在执行查询时进行错误处理。所以，你将有一个功能看起来像

evalExpr :: Expr a -> ExceptT e IO a

而且你可能会执行此有关类型的列相应的检查。

来源

2016-11-18 18:43:56 Alec

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

回答

相关问题