固定長度和類型文字列表

我想在Haskell中定義一個固定長度列表的類型。當我使用標準方式將自然數編碼爲一元類型時，一切正常。但是，當我嘗試在GHC的文字類型上創建所有內容時，我遇到了很多問題。固定長度和類型文字列表

我在所需的列表類型的第一槍是

data List (n :: Nat) a where 
    Nil :: List 0 a 
    (:>) :: a -> List n a -> List (n+1) a

不幸的是沒有允許與類型寫一個zip函數

zip :: List n a -> List n b -> List n (a,b)

我可以從減去1解決這個問題類型變量n中的(:>)類型：

data List (n :: Nat) a where 
    Nil :: List 0 a 
    (:>) :: a -> List (n-1) a -> List n a -- subtracted 1 from both n's

接下來，我試圖定義一個附加功能：

append :: List n1 a -> List n2 a -> List (n1 + n2) a 
append Nil  ys = ys 
append (x :> xs) ys = x :> (append xs ys)

不幸的是，GHC告訴我

Couldn't match type ‘(n1 + n2) - 1’ with ‘(n1 - 1) + n2’

添加約束((n1 + n2) - 1) ~ ((n1 - 1) + n2)到簽名，因爲GHC抱怨

不能解決問題

Could not deduce ((((n1 - 1) - 1) + n2) ~ (((n1 + n2) - 1) - 1)) 
from the context (((n1 + n2) - 1) ~ ((n1 - 1) + n2))

現在，我明顯陷入了某種無限循環。

所以，我想知道是否有可能使用類型文字來定義固定長度列表的類型。我是否甚至爲了這個目的而監督一個圖書館？基本上，唯一的要求是我想寫一些像List 3 a而不是。

來源

2015-04-23 Martin Huschenbett

您可以找到有關輸入電平在Hasochism紙張矢量長度相關的問題的一些討論：https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism。 pdf – chi

「哈索奇」聽起來很誘人。儘管如此，我仍會試一試。謝謝。 –

在附加'Nat'的正常列表周圍創建一個新類型的包裝器可能更容易，類似於'Linear.V'的方式。您可以在一個模塊中定義幾個基元，並隱藏構造函數以確保安全。 – cchalmers

這不是一個真正的答案。

使用https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2，這

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} 

import GHC.TypeLits 

data List (n :: Nat) a where 
    Nil :: List 0 a 
    (:>) :: a -> List n a -> List (n+1) a 

append :: List n1 a -> List n2 a -> List (n1 + n2) a 
append Nil  ys = ys 
append (x :> xs) ys = x :> (append xs ys)

...編譯，所以很明顯它是正確的。

來源

2015-04-23 14:22:45 Sarah

極好的發現。 –

我根本不知道類型檢查器的插件，但是它的工作非常好。謝謝。 –

類型級數字文字還沒有一個我們可以進行歸納的結構，而內置的約束求解程序只能找出最簡單的情況。目前最好堅持佩諾諾自然。

但是，我們仍然可以使用文字作爲句法糖。現在

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

import qualified GHC.TypeLits as Lit 

data Nat = Z | S Nat 

type family Lit n where 
    Lit 0 = Z 
    Lit n = S (Lit (n Lit.- 1))

你可以寫List (Lit 3) a而不是。

來源

2015-04-23 14:14:25

我也有過類似的想法，但是使用'UndecidableInstances'總會讓我害怕。然後使用另一個類型同義詞，我甚至可以到達'List 3 a'。 –

這裏的類型家庭明顯終止，所以'UndecidableInstances'沒有問題。即使在一般情況下，我也不覺得它真的很可怕。如果我們意外地編寫了不同的類型級代碼，我們幾乎總是會得到上下文深度限制錯誤。我們實際上可以得到GHC循環的情況非常罕見，我們可以用Ctr-c輕鬆解決這個問題。 –

固定長度和類型文字列表

回答

相關問題