使用類型Nats創建類型級別列表（在類型級別添加數字時出現問題）

爲了好玩，我想創建一個類型級別列表，知道它有多長。事情是這樣的：使用類型Nats創建類型級別列表（在類型級別添加數字時出現問題）

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeOperators #-} 

import GHC.TypeLits 

data family TypeList a (n::Nat) 

data instance TypeList a (0) = EmptyList 
data instance TypeList a (1) = TL1 a (TypeList a (0)) 
data instance TypeList a (2) = TL2 a (TypeList a (1)) 
data instance TypeList a (3) = TL3 a (TypeList a (2))

但是，我想，當然它推廣到類似：

data instance TypeList a (n) = TL3 a (TypeList a (n-1))

但是，這會產生錯誤：

TypeList.hs:15:53: parse error on input `-' 
    Failed, modules loaded: none.

的另一種嘗試：

data instance TypeList a (n+1) = TL3 a (TypeList a (n))

此外基因錯誤率：

Illegal type synonym family application in instance: n + 1 
    In the data instance declaration for `TypeList'

我假設這樣的事情必須是可能的。這是絕對有可能使用符號：

data Zero 
data Succ a

但我不能弄清楚更好看的版本。

來源

2012-12-16 Mike Izbicki

類型級Nat改進已降落在GHC 7.8中，現在可以實現了！使用

{-# LANGUAGE DataKinds, KindSignatures #-} 
{-# LANGUAGE TypeFamilies, TypeOperators #-} 

import GHC.TypeLits 

data family List (n :: Nat) a 
data instance List 0 a = Nil 
data instance List n a = a ::: List (n - 1) a 

infixr 8 :::

List是一樣自然的任何[]式的數據結構，你會寫自己：

λ. :t 'a' ::: 'b' ::: 'c' ::: Nil 
'a' ::: 'b' ::: 'c' ::: Nil :: List 3 Char

來源

2014-04-03 01:12:33 cdk

當我嘗試在7.8中使用類型級別的Nat時，我遇到的問題是，雖然它現在適用於固定的有限Nats（例如，它可以計算出'List（0 +（1 + 1 + 1）））'是'List 3 Char'），當你試圖編寫像'<++> :: List na - > List ma - > List（n + m）a'這樣的泛型操作時，你會得到像'Could not從上下文（n〜（n1 + 1））中推導出（（（（n1 + m）+ 1）〜（n + m））。因此，它似乎還需要更多的工作才能真正取代基於Zero/Succ的方法 - 儘管我遠離專家，所以也許我錯過了一些東西。 – Ben

由於他們在GHC 7.6中，輸入級Nats不會讓你做這種事情。目前，0 :: Nat和1 :: Nat類型之間或多或少沒有任何關係，儘管名稱的含義如何（不同於您的Zero和Succ Zero，您可以使用它們做些有用的事情）。在未來的GHC版本中這會更好。

來源

2012-12-16 04:40:46 shachaf

是，該計劃爲7.8，或者是不完全闡明瞭嗎？ –

使用類型Nats創建類型級別列表（在類型級別添加數字時出現問題）

回答

相關問題