在这个类型化的λ演算宇宙中，你如何构造n元积类型和求和类型？

Question

这里是我遇到问题的代码：

{-# LANGUAGE GADTs, LANGUAGE DataKinds #-} 

-- * Universe of Terms * -- 

type Id = String 

data Term a where 
   Var :: Id -> Term a
   Lam :: Id -> Type -> Term b -> Term (a :-> b)
   App :: Term (a :-> b) -> Term a -> Term b 
   Let :: Id -> Term a -> Term b -> Term b 

   Tup :: Term a -> Term b -> Term (a :*: b)   -- * existing tuple
   Lft :: Term a -> Term (a :+: b)   -- * existing sum 
   Rgt :: Term b -> Term (a :+: b)

   Tru :: Term Boolean
   Fls :: Term Boolean
   Bot :: Term Unit

-- * Universe of Types * --

data Type = Type :-> Type | Type :*: Type | Type :+: Type | Boolean | Unit

所以我想将Tup扩展到可以定义任意数量的参数，与sum相同。但涉及到列表的公式会将最终项限制为一种类型的a：

因此，我希望能够对Tup和sum函数进行扩展，使它们能够适用于任意数量的参数。然而，如果涉及到列表的表达式，最终的结果可能会被限制为特定类型的a。

Sum :: [Term a] -> Term a 

我可以只删掉a标签，然后做这样的事情：

Sum :: [Term] -> Term

但这样我就失去了我试图表达的东西。

那么，我如何在不损失表现力的情况下表达多态项？

- xiaolingxiao

---

这看起来非常像您想要对不同类型的“Term”进行求和，但问题的标题表明您想要形成一个总和类型。那么您实际上想要做什么？ - Tom Ellis

为什么不直接使用二元求和和乘积呢？你的Tup已经形成了一个乘积类型。同样地，你可以为二元求和类型创建 Lft :: Term a -> Term (a :+: b) 和 Rgt :: Term b -> Term (a :+: b)。当然，还需要将 Type :+: Type 加入到你的类型集合中。 - kosmikus

像@kosmikus所说的那样，如果您想要一个单位来表示您的产品，可以添加Unt :: Term Unit。 - augustss

@kosmikus，我更新了标题以更好地反映我的问题。 - xiaolingxiao

@chibro2，但是现在你需要两种类型的证人来构建一个Sum；这不是通常的定义方式。通常Sum要求任一类型的证人。因此，kosmikus的解决方案需要Lft和Rgt。 - Sassa NF

Answer 1

在Haskell的类型系统中，对于“列表”这个概念进行操作有些棘手，但是可以实现。作为起点，如果你限制自己只使用二元积和二元和（就我个人而言，我会坚持这种方式），那么这将变得非常容易：

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

import Prelude hiding (sum) -- for later

-- * Universe of Terms * -- 

type Id = String 

data Term :: Type -> * where 
   Var :: Id -> Term a
   Lam :: Id -> Type -> Term b -> Term (a :-> b)
   App :: Term (a :-> b) -> Term a -> Term b 

   Let :: Id -> Term a -> Term b -> Term b 
   Tup :: Term a -> Term b -> Term (a :*: b) -- for binary products
   Lft :: Term a -> Term (a :+: b) -- new for sums
   Rgt :: Term b -> Term (a :+: b) -- new for sums
   Tru :: Term Boolean
   Fls :: Term Boolean
   Uni :: Term Unit -- renamed

-- * Universe of Types * --

data Type = Type :-> Type | Type :*: Type | Type :+: Type | Boolean | Unit | Void
  -- added :+: and Void for sums

为了构建任意长度的和类型，我们需要一个术语环境。这是一个由其中术语类型索引的异构列表：

data Env :: [Type] -> * where
   Nil   :: Env '[]
   (:::) :: Term t -> Env ts -> Env (t ': ts)

infixr :::

我们可以使用类型族将类型列表折叠成二元积类型。 或者，我们可以在Type宇宙中添加类似于Product [Type]的内容。

type family TypeProd (ts :: [Type]) :: Type
type instance TypeProd '[]       = Unit
type instance TypeProd (t ': ts) = t :*: TypeProd ts

< p > prod 函数将这样的环境折叠为 Tup 的应用程序。同样，您还可以将 Prod 添加为此类型的构造函数到 Term 数据类型中。

prod :: Env ts -> Term (TypeProd ts)
prod Nil        = Uni
prod (x ::: xs) = x `Tup` prod xs

任意长度的求和仅需要一个元素来注入，但需要一个标签来指示要注入到哪种类型的总和中：

data Tag :: [Type] -> Type -> * where
   First :: Tag (t ': ts) t
   Next  :: Tag ts s -> Tag (t ': ts) s

再次，我们有一个类型族和一个构建这种类型族的函数：

type family TypeSum (ts :: [Type]) :: Type
type instance TypeSum '[]       = Void
type instance TypeSum (t ': ts) = t :+: TypeSum ts

sum :: Tag ts t -> Term t -> Term (TypeSum ts)
sum First    x = Lft x
sum (Next t) x = Rgt (sum t x)

当然，有很多变化或概括是可能的，但这应该能给你一个想法。

- kosmikus