你如何在这个类型化的lambda微积分宇宙中制定n元产物和求和类型？

这里就是我有一个问题的代码：要在任意多的参数定义你如何在这个类型化的lambda微积分宇宙中制定n元产物和求和类型？

{-# 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] -> Term a

我可以摆脱a，并做一些事情，如：

Sum :: [Term] -> Term

但后来我失去了很我想表达的东西。

那我该如何表达一些多态词汇而不会损失表达力呢？

来源

2014-01-20 chibro2

这看起来很像你想总结不同类型的术语，但问题的标题表明你想要形成一个总和*类型*。那么你究竟想要做什么？ –

为什么不使用二元和和产品？你的“Tup”已经在形成一种产品类型。同样，对于二进制和类型，您可以有'Lft :: Term a - > Term（a：+：b）'和'Rgt :: Term b - > Term（a：+：b）'。当然，添加'Type：+：Type'到你的宇宙类型。 – kosmikus

@kosmikus说了什么，如果你想要一个产品的单位，可以加上'Unt :: Term Unit'。 – augustss

对于“列表”，使用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 Universe中添加诸如Product [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)

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

来源

2014-01-20 17:24:28 kosmikus

你如何在这个类型化的lambda微积分宇宙中制定n元产物和求和类型？

回答

相关问题