你如何在这种类型的lambda演算世界中制定n-ary乘积和和类型？

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相同.但是涉及列表的公式会将最终的术语限制为一种类型:

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

任意长度的和只需要一个元素来注入,但是需要一个标记来指示注入它的总和的类型:

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)

当然,可能有很多变化或概括,但这应该给你一个想法.