是否有可能對同一構造函數有不同的行爲？

我在寫一個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

是否有可能對同一構造函數有不同的行爲？

回答

相關問題