在Haskell中生成Haskell類型的設備（「second order Haskell」）？

Question

如果這個問題有點模糊，請事先道歉。這是一些週末白日夢的結果。

使用Haskell的精彩類型系統，將數學（特別是代數）結構表示爲類型類是令人高興的。我的意思是，只要看看numeric-prelude！但是，在實踐中利用這種美妙的類型結構對我來說似乎總是很困難。

你必須表達該v1和v2是向量空間V的元素和w是向量空間W的一個元件的一個很好的，類型系統的方法。類型系統允許您編寫一個程序，添加v1和v2，但不包括v1和w。大！但在實踐中，您可能想要使用潛在的數百個矢量空間，並且您當然不想創建類型V1，V2，...，V100並將它們聲明爲向量空間類型類的實例！或者，也許你從現實世界中讀取了一些數據，導致符號爲a,b和c - 您可能想要表示這些符號上的自由矢量空間確實是一個向量空間！

所以你卡住了吧？爲了在科學計算設置中執行很多你想要處理矢量空間的事情，你必須放棄你的類型系統，方法是先向量空間類型類別，然後讓函數執行運行時兼容性檢查。你應該嗎？難道不可能使用Haskell純粹的功能來編寫一個程序來生成所需的所有類型，並將它們插入到真正的程序中嗎？這種技術是否存在？通過一切手段指出，如果我只是在這裏忽略一些基本的東西（我可能是）:-)

編輯：剛纔我發現fundeps。我將不得不考慮他們與我的問題有何關係（有關這方面的啓發性評論，我們將不勝感激）。

Answer 1

Template Haskell允許這個。 wiki page有一些有用的鏈接;特別是Bulat'stutorials。

頂層聲明語法是你想要的。通過鍵入：

mkFoo = [d| data Foo = Foo Int |] 

你生成一個模板哈斯克爾拼接（如編譯時的功能），將剛剛通過插入線$(mkFoo)創建data Foo = Foo Int聲明。

雖然這個小例子不是太有用，但您可以提供一個參數給mkFoo來控制您想要的多少個不同的聲明。現在，$(mkFoo 100)將爲您生成100個新的數據聲明。您也可以使用TH來生成類型類實例。我的adaptive-tuple包是一個非常小的項目，它使用Template Haskell來做類似的事情。

另一種方法是使用Derive，它會自動派生類型實例。如果你只需要這些實例，這可能會更簡單。

Answer 2

Haskell中還有一些簡單的類型級編程技術。一個典型的例子如下：

-- A family of types for the natural numbers 
data Zero 
data Succ n 

-- A family of vectors parameterized over the naturals (using GADTs extension) 
data Vector :: * -> * -> * where 
    -- empty is a vector with length zero 
    Empty :: Vector Zero a 
    -- given a vector of length n and an a, produce a vector of length n+1 
    Cons :: a -> Vector n a -> Vector (Succ n) a 

-- A type-level adder for natural numbers (using TypeFamilies extension) 
type family Plus n m :: * 
type instance Plus Zero n = n 
type instance Plus (Succ m) n = Succ (Plus m n) 

-- Typesafe concatenation of vectors: 
concatV :: Vector n a -> Vector m a -> Vector (Plus n m) a 
concatV Empty ys = ys 
concatV (Cons x xs) ys = Cons x (concatV xs ys) 

花點時間把它。我認爲它是相當神奇的，它的工作原理。

但是，Haskell中的類型級編程是在feature-uncanny-valley中 - 僅僅足以讓人們注意到你不能做多少事情。諸如Agda，Coq和Epigram這樣的依賴型語言將這種風格設置爲極限和全功能。

模板Haskell更像通常的LISP宏代碼生成風格。你寫一些代碼來編寫一些代碼，然後你說「OK在這裏插入生成的代碼」。與上述技術不同的是，您可以用這種方式編寫任何可計算的指定代碼，但是您沒有像上面的concatV中看到的那樣進行非常普遍的類型檢查。

所以你有幾個選擇去做你想做的。我認爲元編程是一個非常有趣的領域，在某些方面還很年輕。玩得開心。 :-)