Haskell相當於非類型的C++模板

我的一般理解是，Haskell類型類與C++模板共享一些概念上的相似性 - 也就是說，您可以定義通過類型進行參數化的函數或類型。但是，C++模板的一個有用特性是，您還可以擁有非類型的模板參數。例如，Wikipedia有一個great example關於如何創建編譯時間因子。Haskell相當於非類型的C++模板

我理想上喜歡在Haskell做同樣的事情...我幾乎可以用DataKinds擴展。以一個矢量的典型例子爲例，它編碼了它的長度（取自here）。

data Nat = Ze | Su Nat 

data Vec :: * -> Nat -> * where 
    Nil :: Vec a Ze 
    Cons :: a -> Vec a n -> Vec a (Su n)

我想能夠載體的爲「降級」的類型級「納特」回落到值電平（可能與ScopedTypeVariables），所以我可以用它作爲一個可以使用C++非類型的模板參數作爲常量值。 GHC.TypeLits類似於KnownNat類中的一些hackery（它僞造每個具體文字的實例），但我顯然不能在Haskell中自己寫這個。

我覺得我想要的東西是不可能的，但我想直覺一下爲什麼它不可能。

我覺得依賴類型潛伏...

來源

2016-01-22 Alec

你可以自己做，但效率不高。數據Nat = Z | S Nat'。 'Natty類（n :: Nat），其中natty :: proxy n - > Nat'和一個用於'Z'的實例，另一個用於'S n'。 – dfeuer

當'Vec（）'是'Nat'的單例時，每個人都會建議OP使用單身......這意味着你不需要寫一個單例，因爲'Vec'類型的歸納給了你所有的力量納特的單身漢。您還可以使用簡單函數'len：Vec x n - > Integer來獲取矢量類型級別長度的值級表示。 len無= 0; len（Cons _ xs）= 1 + len xs'。 – user2407038

不要忘記我們有類型族，可以與'UndecidableInstances'結合使用。例如。 http://hackage.haskell.org/package/type-level-numbers – chi

的技術做到這叫做singleton types（該鏈接還鏈接到一個庫來支持這一點）。

核心思想是創建一個參數化類型構造函數，以便在類型值和類型參數之間存在一對一的對應關係。以下是上述鏈接中引用的第一篇論文的簡化示例。

data SBool (a :: Bool) where 
    STrue :: SBool 'True 
    SFalse :: SBool 'False

現在有SBool 'True即STrue類型只有一個值。我們還通過GADT魔術知道，當我們在SBool a上進行模式匹配時，得到STrue，然後a ~ 'True。現在，返回值，我們使用普通機制來根據type：type類來選擇一個值。

class FromSBool (a :: 'Bool) where 
    fromSBool :: SBool a -> Bool 

instance FromSBool 'True where 
    fromSBool STrue = True 

instance FromSBool 'False where 
    fromSBool SFalse = False

這是一個非常簡單的例子，但圖書館引用進入更多細節的論文，或者您可以使用該庫。你是正確的，類型級別的自然有些神奇。一個相關的庫是reflection包，它允許你將一個值放入一個類型並在稍後返回。

如果您對某些理論感興趣，您可能也對該論文Hasochism感興趣。

來源

2016-01-22 09:40:56

謝謝！這看起來確實很酷。除非有人有更好的解決方案，否則我會很快接受你的答覆。 – Alec

Haskell相當於非類型的C++模板

回答

相關問題