如何在Haskell中遞歸地定義一個類型序列？

具體是什麼我想要做的就是定義，每個正整數n，a型層級n的列表。由此我的意思是看起來有點像這樣（但可能不完全）。首先，對於任何類型的a讓List a是[a]。（這個我知道怎麼做的。）現在，我想如何在Haskell中遞歸地定義一個類型序列？

IteratedList 0 a = a

IteratedList n a = List (IteratedList (n-1) a)

因此，例如，IteratedList 3 a是[[[a]]]。

我想要這樣做的原因是我想編寫一個解析器，它可以通過識別左括號，挑選出一堆n-1級別的列表，然後識別右括號。但我不知道如何爲解析器創建適當的類型聲明。

也許我處理事情的方式不對。如果是這樣，那麼正確的方法是什麼？

後來添加的。非常感謝以下有用的答案。最後，（i）使用像嵌套列表概念和（ii）n.m.這表明，我幾乎可以肯定沒有需要使用一個（我懷疑的一半），我意識到，我可以實現我想要與我確實沒有需要嵌套列表類型的簡單方法分析器。有用的教訓。

來源

2014-06-25 user15553

是否希望解析結果的類型取決於解析的字符串？您需要一種具有相關類型的語言來實現這一點。 Haskell不是其中之一。請注意，你並不需要它。 –

爲什麼你想在類型級別做到這一點？ –

您將無法編寫解析器，而解析器的類型取決於被解析的內容，Haskell的類型系統無法正常工作。您必須提前知道該類型。 – Dan

我不完全推薦這個，但是你可以使用新型的水平字面Nat機械在GHC 7.8實現這一目標。

{-# LANGUAGE KindSignatures, TypeFamilies #-} 

import GHC.TypeLits 

type family IteratedList (n :: Nat) a where 
    IteratedList 0 a = [a] 
    IteratedList n a = IteratedList (n - 1) [a]

這使得使用密閉型家族的遞歸超過Nat的結構中，添加各它遞歸時間的[]類型級別層。

來源

2014-06-25 16:46:05 cdk

這是棘手的，但這樣做，能夠與某些類型的水平的黑客。可悲的是它比你想要的更復雜。

我避免封閉式的家庭因此這將GHC 7.6編譯和高達

{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeFamilies #-} 

import Data.Proxy 

data Nat = S Nat | Z -- Type level natural numbers, Z means zero, S n means n + 1 
type family IteratedList (n :: Nat) a 
type instance IteratedList Z a  = [a]    -- Base case 
type instance IteratedList (S n) a = [IteratedList n a] -- Inductive step

注意，這個工程完全一樣數學歸納法？我們「證明」什麼IteratedList是當n是Z，然後我們可以「證明」n是S n使用IteratedList n a時它是什麼。

這實際上可以採取相當深層次的，我們很快開始撞到差GHC的開放型家庭的範圍，並最終需要GHC 7.8。

爲了幫助GHC的類型檢查有了這一切，我們需要提供所謂Proxy秒。這些只是簡單的數據類型，我們用一個幻像類型變量來表示類型檢查器的有用內容。

下面是我們稍後使用的幫助函數，其中Proxy包含一個大於零的數字，並返回一個數字減1的代理。

predProxy :: Proxy (S n) -> Proxy n 
predProxy = reproxy

現在我們使用類型類跨 IteratedList小號推廣業務。這些類基本上像通過歸納一樣工作。例如，以下是在IteratedList內製作單個元素的類。

class Single (n :: Nat) a where 
    single :: Proxy n -> a -> IteratedList n a 
instance Single Z a where 
    single _ = (:[]) 
instance Single n a => Single (S n) a where 
    single p a = [single (predProxy p) a]

需要的Proxy n參數來幫助GHC的類型檢查明白這是怎麼回事，因爲否則會產生很多新的類型變量，然後固執地不統一它們。據推測，這有一個聰明的原因。

請注意，類型類的兩個實例看起來非常類似於我們如何定義IteratedList？一個用於Z，然後是一個歸納步驟。

至於在運行時構造這個..從技術上講，這全部都是基於類型同義詞，所以你實際上並不需要一個轉換例程，只是爲了構建列表。棘手的一點是，你需要將這個n放在存儲器或CPS代碼中，這樣你就可以有1個返回類型。

否則你的返回類型將取決於你的輸入，你不能表達一些如此複雜的GHC。

你能想象像

buildIteratedList :: String -> (forall n. IteratedList n a -> r) -> r

但很快就變得相當可怕以來每操作需要是一個類型類感應GOOP，以便在n要普及工作。

我建議只是做一些簡單的像

data Nested a = Elem a 
       | List [Nested a]

，做運行時檢查..如果沒有相關的類型，這似乎很不可行了我。

來源

2014-06-25 16:52:11 jozefg

我同意玫瑰樹般的東西看起來像最好的選擇（到目前爲止）。其實我只是想推薦一朵玫瑰樹。儘管如此，我還是建議使用封閉類型的家庭，因爲不需要開放，GHC 7.8現在已經正式推出。但是我仍然會建議像'Nested'這樣的方式。 –

我試過這個，並以一個錯誤消息告訴我它不能匹配類型爲Nested a的類型[Nested a]。我一直希望它們會是一樣的（除了一個物體不屬於[Nested a]）。 – user15553

@ user15553嗯，這取決於你在做什麼，但有一個函數可以幫助：'List :: [Nested a] - > Nested a' –

我不知道你想用你的解析表示的列表來做什麼，所以很難給出一個「一般」的答案，所以我會編一個列表並解析它，並且你可以告訴我，如果這是你在找什麼。

import Data.List.Split 
import Data.List(span) 

data NestedList a = NestedList{ nesting :: Int, elems :: [a] } 
    deriving (Show, Eq) 

testlist = "[ [ [1,2], [3,4], [5,6], [1] ], [ [9] ] ]" 

parseList :: Read a => String -> NestedList [a] 
parseList = merge . go 0 
    where go n []  = [] 
      go n (x:xs) = case x of 
      '[' -> go (n + 1) xs 
      ']' -> go (n - 1) xs 
      ',' -> go n xs 
      ' ' -> go n xs 
      _ -> NestedList n (map read $ splitOn "," elems) : go n rest 
         where (elems, rest) = span (`notElem` "[]") (x:xs) 
      merge [] = NestedList 0 [] 
      merge (NestedList n xs:ns) = 
      let next = elems (merge ns) 
      in NestedList n (xs:next)

這絕不是完美的，尤其是因爲這三嵌套9被解釋爲「只是一個元素，」但它是一個開始。

*> parseList testlist :: NestedList [Int] 
*> NestedList {nesting = 3, elems = [[1,2],[3,4],[5,6],[1],[9]]}

的想法基本上是他們跟蹤我們有多深解析樹時去的，建了一堆嵌套列表的過程中，再綜合企業到一個大的嵌套列表。再次，這不是完美的，但它是一個開始（和嘗試將依賴類型輸入到Haskell中的方法不同）;）

來源

2014-06-25 20:04:51

如何在Haskell中遞歸地定義一個類型序列？

回答

相關問題