Как вы формулируете 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 для определения по произвольно многим аргументам, то же самое с суммой. Но формулировка, включающая списки, будет ограничивать окончательный термин одним типом a:

Sum :: [Term a] -> Term a

Я мог бы просто избавиться от a и сделать что-то вроде:

Sum :: [Term] -> Term

Но потом я теряю то, что я пытаюсь выразить.

Итак, как выразить некоторый полиморфный термин без потери выразительности?

Ответы

Ответ 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)

Конечно, возможны множество вариантов или обобщений, но это должно дать вам идея.