Вот код, в котором у меня проблема:
{-# 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
Но потом я теряю то, что я пытаюсь выразить.
Итак, как выразить некоторый полиморфный термин без потери выразительности?