haskell - 在这个类型化的 lambda 演算宇宙中，您如何制定 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 相同。但是涉及列表的公式会将最终 Term 限制为一种类型的 a:

Sum :: [Term a] -> Term a 

我可以摆脱 a并执行以下操作:

Sum :: [Term] -> Term

但后来我失去了我试图表达的东西。

那么如何在不损失表达性的情况下表达一些多态术语呢？

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 :::

然后，我们使用类型族将类型列表折叠成二进制产品类型。
或者，我们可以添加类似 Product [Type] 的内容到 Type宇宙。

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

prod函数将这样的环境折叠到 Tup 的应用程序中.再一次，你
也可以添加 Prod作为 Term 的这种类型的构造函数数据类型。

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

任意长度的和只需要一个元素来注入(inject)，但需要一个标签来表示
注入(inject)哪种类型的总和:

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)

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