代码之家 › 专栏 › 技术社区 › user3368561

定义具有最少固定点、总和和产品类型的列表

fixpoint-combinators type-theory haskell

user3368561 · 技术社区 · 7 年前

我只想使用此类型定义定义列表:

data Unit = Unit
data Prod a b = P a b
data Sum a b = L a | R b
newtype Mu f = Mu (forall a . (f a -> a) -> a)

我成功地定义了自然数如下:

zeroMu = Mu $ \f -> f $ L Unit
succMu (Mu g) = Mu $ \f -> f $ R $ g f

我知道如何借助额外的数据类型定义列表:

data ListF a x = NilF | ConsF a x
nilMu' = Mu $ \f -> f $ NilF
consMu' x (Mu g) = Mu $ \f -> f $ ConsF x $ g f

我能得到的“更好”是这个,但它不进行类型检查(预期的类型是μl(1+(a*l)):

nilMu = Mu $ \f -> f $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ R $ P x $ g f

我如何定义 nilMu 和 consMu 只使用以前定义的类型及其构造函数?

编辑

正如@chi answer所解释的,可以定义 newtype 如下:

newtype F a x = F (Sum Unit (Prod a x))
nilMu = Mu $ \f -> f $ F $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ F $ R $ P x $ g f

它进行类型检查,但需要定义新类型。

这个问题的目的是用单位、积、和和递归类型扩展一个简单类型的组合逻辑。前三种类型很容易实现引入7个新的组合器( unit , pair , first , second , left , right , case )递归类型似乎也很容易实现,只需添加一个类型构造函数组合器 mu 但是,由于这些Questoin显示没有足够的语言结构就不够灵活。

这个问题有解决办法吗?有递归类型的组合逻辑可供参考吗?

1 回复 | 直到 5 年前

chi 7 年前

你不能没有额外的 data 或 newtype 在哈斯克尔。

要做到这一点,人们需要写

nilMu :: Mu (\l -> S (P a l) ())
consMu :: a -> Mu (\l -> S (P a l) ()) -> Mu (\l -> S (P a l) ())

但是Haskell不允许这样的类型级函数。 Mu 只能应用于类的类型构造函数 * -> * 不是同一类型的类型级函数。

nilMu :: Mu (F a)
consMu :: a -> Mu (F a) -> Mu (F a)

哪里 F a 定义为附加类型

newtype F a x = F (S (P a x) ())

由于Haskell不允许类型级函数的原因,请考虑

assuming foo :: f a -> f Char
infer    foo True :: ???

有人可能会说 foo True , True 是一个 Bool ,所以我们可以推断 f = \t->t 和 a = Bool . 结果是 foo True :: (\t->t) Char = Char .

有人可能会说我们可以推断 f = \t->Bool 和 a = String ,结果是 foo True :: (\t->Bool) Char = Bool

总的来说,我们不喜欢这样。我们希望通过模式匹配来进行类型推理。 f 和 a 与实际类型相反。为此,我们两个都要 f 和 一 有记者“显而易见” 名称在实际类型中。

为了它的价值,你可以在依赖类型语言(如coq、agda、idris等)中执行此操作。在这种情况下,类型推断不会在以下代码上工作 真实的 以上,因为 f 无法推断。更糟的是,在这些语言中,如果 bar :: f a -> ... 我们打电话 bar [True] 然后 f 无法推断 [] 因为这不是唯一的解决方法(尽管它们的一般问题是不可判定的),但它们确实有很好的启发式算法,这通常是有效的。

推荐文章

Azathoth · 当使用过滤器不删除任何案例时,涉及空列表的案例不会编译

3 年前

Ethan Smallwood · Haskell从列表中的记录获取数据

3 年前

trpnd · 如何定义由两个任意单声道变压器组成的单声道变压器?

3 年前

Delfin · Haskell从do符号到Applicative符号的传递(第2部分)

3 年前

Fabus1184 · Haskell mapM_不打印

3 年前

Gotthold · 基于范数约束向量的类型

3 年前

dmcdo · 有没有一种干净的方法可以在一个表达式中得到列表的开头和结尾?

3 年前

jian · haskell将另一个函数用作输入参数

3 年前

Jocafrei · 用Haskell函数实现最大公约数函数

7 年前

pcoppi · 尝试在Haskell和根据-Wall编写函数时,我需要一个匹配(\u:\ u:\ u)的模式。这个模式意味着什么,为什么我需要它?

7 年前