避免類型級別上的類別限制

我使用GHC.TypeLits模塊中的Nat類型，它承認程序員接口應該在單獨的庫中定義。在任何情況下，GHC.TypeLits具有類KnownNat與類功能natVal其中編譯時Nat轉換成運行時Integer。還有它增加了編譯時間Nat個類型功能(+)。避免類型級別上的類別限制

的問題是，鑑於(KnownNat n1, KnownNat n2)，GHC不能推導出KnownNat (n1 + n2)。

這導致在任何需要的時候我添加型水平土黃要添加的約束的爆炸。

一種替代方法是定義自然數自己就像這樣：

data Nat = Zero | Succ Nat

也許使用圖書館像type-natural。但似乎傻不使用其內置到GHC的納茨，這也可以讓您很好的類型（即0，1）使用文字數字，而不必定義：

N0 = Zero 
N1 = Succ N0 
etc...

反正是有解決這個與GHC KnownNat約束是否需要在所有地方？或者我應該忽略GHC.TypeLits模塊來解決我的問題？

來源

2017-01-10 Clinton

您可能對[此問題]感興趣（https://stackoverflow.com/questions/41492754/could-not-deduce-knownnat-in-two-existentials-with-respect-to-the-singletons-lib/41496362）和相應的答案。 – gallais

這GHC類型檢查插件不正是（派生的「複雜」 KnownNat從其他的約束條件已發售）：https://hackage.haskell.org/package/ghc-typelits-knownnat

如果「類型檢查器插件」，聽起來有點嚇人（它確實對我來說是第一次），它的使用非常簡單。只需將它添加在你的包文件的依賴（或小集團安裝）像任何其他包，然後可以添加：

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

到您的源文件的開始（很像LANGUAGE編譯），或將其添加作爲包文件的全局選項。

還有由同一作者這是非常有用的，以及與typelit納茨工作另一個插件：https://hackage.haskell.org/package/ghc-typelits-natnormalise。這一個是能夠推斷出NAT類型表達式GHC自身對放棄的平等：之類的東西n + (m + 1) ~ (n + 1) + m是拿出所有的時間時GHC正試圖證明「預期」和「實際」類型匹配。

來源

2017-01-10 05:39:35 Ben

避免類型級別上的類別限制

回答

相關問題