如何在Haskell中递归定义一系列类型？

Question

具体来说,我想要做的是为每个正整数n定义级别为n的列表的类型.我的意思是看起来有点像这样(但可能不完全是).首先,对于任何类型的a让List a是[a].(我知道怎么做.)现在我想

IteratedList 0 a = a

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

所以,例如,IteratedList 3 a将是[[[a]]].

我想要这个的原因是我想编写一个解析器,它可以通过识别开括号,挑出一堆级别为n-1的列表,然后识别结束括号来挑选级别n的列表.但我不知道如何为解析器做出适当的类型声明.

也许我会以错误的方式处理事情.如果是这样,那么正确的方法是什么？

稍后补充.非常感谢下面的有用答案.最后,由(i)难以使用嵌套列表概念之类的东西和(ii)nm的评论表明我几乎肯定不需要使用一个(我怀疑的一半),我意识到我可以通过简单的方式实现我的解析器所需的功能,确实不需要嵌套列表的类型.有用的经验教训.

Answer 1

这很棘手,但可以使用某种类型级别的黑客攻击.可悲的是,它比你想要的更复杂.

我避免使用封闭类型系列,因此这将使用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的类型检查器完成所有这些,我们需要提供所谓的Proxys.这些只是带有幻像类型变量的简单数据类型,我们用它来表示类型检查器的有用内容.

这是我们稍后使用的辅助函数,它接受一个Proxy大于零的数字,并返回一个数字减1的代理.

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

现在我们使用类型类来概括IteratedLists中的操作 .这些类基本上像归纳一样工作.例如,这是在一个内部生成单个元素的类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]

并且做运行时检查..没有依赖类型,这对我来说似乎是不可行的.