是否有可能对同一构造函数有不同的行为？ [英] is it possible to have different behaviors for the same constructor?

问题描述

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

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

  SELECT $ [ColumnNamefirst_name`AS`name]`FROM` TABLE people.csv`WHERE`（ColumnNameage`Gte` LiteralInt 40）
  

（b）
$ b

 （ColumnNameage`Gte` LiteralInt 40）
 
 code> 

这应该通过类型检查器。但是，说年龄不包含可以表达为 LiteralInt 的东西。

所以我想要 Gte 产生类似于 IO Bool 的东西（目前不在意异常处理）。

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

（LiteralInt 40`Gte` LiteralInt 10）我只需要一个布尔。
或类似的东西：
（LiteralInt 40`Gte` LiteralBool True）需要在编译时失败。

因此，我一直在研究数据家族和GADT，并且已经消除了许多死胡同，如果我解释它们就会混淆局面。

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

Gte 产生类似于的东西， IO Bool （目前不在意异常处理）。

但我并不总是需要 Gte 产生 IO Bool 。

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

或类似的内容：（LiteralInt 40`Gte` LiteralBool True）需要在编译时失败。

现在 更合理。如果您决定走这条路，您甚至可以使用新的 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 
  

然后，以下代码将全部编译：

  ColumnNameage`Gte` LiteralInt 40 
 LiteralInt 40`Gte` LiteralInt 10 
（LiteralInt 40`Add` ColumnNameage）`Gte `LiteralInt 10 
  

以下不会：

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

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

如果您在编译时知道您的模式并且想要执行大量TYPE-两轮牛车。更简单的解决方案就是在执行查询时进行错误处理。所以你会看到类似于
$ b

  evalExpr :: Expr a  - >除了这种情况以外，你可能会在这里对列的类型进行适当的检查。  
 $ p 
 
 
 p> 
I'm writing an SQL interpreter. I need to distinguish between ill-formed expressions at compile time, and run-time errors.

I'll give you an example of something that should be well-formed, but possibly fails at run-time.
SELECT $ [ColumnName "first_name" `AS` "name"] `FROM` TABLE "people.csv" `WHERE` (ColumnName "age" `Gte` LiteralInt 40)
I'd like to focus in on the expression:
(ColumnName "age" `Gte` LiteralInt 40)
This should pass the type checker. But, say "age" did not contain something that could be expressed as a LiteralInt.

So I would want Gte to produce something like IO Bool (not minding exception handling for now).

But I wouldn't always need Gte to produce an IO Bool. In the event I had something like this:

(LiteralInt 40 `Gte` LiteralInt 10) I just need a Bool.
or something like this:
(LiteralInt 40 `Gte` LiteralBool True) needs to fail at compile time.

So, I've been toying around with data families and  GADTs, and have gone down many dead ends that would just serve to confuse the situation if I explicated them. 

Does my problem make sense, and if so is there a path of inquiry I can traverse that will lead to a solution?
解决方案

  
So I would want Gte to produce something like IO Bool (not minding exception handling for now).
  
  
But I wouldn't always need Gte to produce an IO Bool.
That is not possible (nor indeed desirable). Gte will have to always return the same type. Also, you probably want to separate the construction of your query from its execution...

  
or something like this: (LiteralInt 40 `Gte` LiteralBool True) needs to fail at compile time.
Now that is much more reasonable. If you decide to go down that path, you can even customize the type errors GHC reports with the new TypeError feature. However, sticking to a simple example involving just LiteralInt, LiteralBool and Gte, you could do something like the following with just 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
Then, the following would all compile:
ColumnName "age" `Gte` LiteralInt 40
LiteralInt 40 `Gte` LiteralInt 10
(LiteralInt 40 `Add` ColumnName "age") `Gte` LiteralInt 10
while the following would not:
LiteralInt 40 `Gte` LiteralBool True
LiteralInt 40 `Add` LiteralBool True



  
But, say "age" did not contain something that could be expressed as a LiteralInt.
You could potentially make this also compile time if you knew your schema at compile time and you wanted to do lots of type-hackery. The simpler solution would be just to make the error handling happen when you execute your query. So you would have a function looking something like
evalExpr :: Expr a -> ExceptT e IO a
And you would probably perform the appropriate checks concerning the types of columns here.

                        
这篇关于是否有可能对同一构造函数有不同的行为？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！