Можно ли написать структуру данных или структуры данных, которые представляют только закрытые термины на Haskell или на любом другом языке?

Question

Используя нотацию Де Брёйна, можно определить лямбда-термины как:

data BTerm = BVar Int | BLam BTerm | BApp BTerm BTerm

Или используя обычные обозначения, data Term = Var String | Lam String Term | App Term Term

Эти два типа данных позволяют создавать как закрытые термины, так и термины, содержащие свободные переменные.

Можно ли определить тип данных, который позволяет создавать только закрытые термины. т.е. только такие термины, как: \ xx, \x. хх, \ х. \ у. ху, \ х. \ у. у, \ х. \ у. \ zz(ху)

Answer 1

Вы можете использовать GADT, чтобы сделать список свободных переменных пустым. Свободные переменные могут храниться в списке уровня типа. Ниже я решил использовать индексы Де Брёйна для представления переменных.

Начнем с определения того, как добавить два списка уровней типов:

      {-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, TypeOperators,
    GADTs, ScopedTypeVariables, TypeApplications #-}
{-# OPTIONS -Wall #-}

import GHC.TypeLits
import Data.Proxy

-- Type level lists append
type family (xs :: [Nat]) ++ (ys :: [Nat]) :: [Nat] where
   '[]       ++ ys = ys
   (x ': xs) ++ ys = x ': (xs ++ ys)

Затем мы вычисляем свободные переменные \ t учитывая те из t.

      -- Adjust Debuijn indices under a lambda:
-- remove zeros, decrement positives
type family Lambda (xs :: [Nat]) where
   Lambda '[]       = '[]
   Lambda (0 ': xs) = Lambda xs
   Lambda (x ': xs) = x-1 ': Lambda xs

Наконец наш GADT:

      -- "BTerm free" represents a lambda term with free variables "free"
data BTerm (free :: [Nat]) where
   BVar :: KnownNat n => BTerm '[n]
   BLam :: BTerm free -> BTerm (Lambda free)
   BApp :: BTerm free1 -> BTerm free2 -> BTerm (free1 ++ free2)

Тип для закрытых условий теперь легко определить:

      -- Closed terms have no free variables
type Closed = BTerm '[]

Мы сделали. Напишем несколько тестов. Начнем с Show instance, чтобы иметь возможность напечатать термины.

      showBVar :: forall n. KnownNat n => BTerm '[n] -> String
showBVar _ = "var" ++ show (natVal (Proxy @n))

instance Show (BTerm free) where
   show t@BVar       = showBVar t
   show (BLam t)     = "\\ " ++ show t
   show (BApp t1 t2) = "(" ++ show t1 ++ ")(" ++ show t2 ++ ")"

А вот пара тестов:

      -- \x. \y. \z. z (x y)
-- Output: \ \ \ (var0)((var2)(var1))
test1 :: Closed
test1 = BLam (BLam (BLam (BApp z (BApp x y))))
   where
   z = BVar @0
   y = BVar @1
   x = BVar @2

-- \x. \y. x y (\z. z (x y))
-- Output: \ \ ((var1)(var0))(\ (var0)((var2)(var1)))
test2 :: Closed
test2 = BLam (BLam (BApp (BApp x' y') (BLam (BApp z (BApp x y)))))
   where
   z  = BVar @0
   y  = BVar @1
   x  = BVar @2
   y' = BVar @0
   x' = BVar @1

Answer 2

Если вы хотите закодировать его в какой-либо форме, близкой к произвольным лямбда-выражениям, я подозреваю, что для отслеживания текущей глубины лямбда потребуется некоторое программирование на уровне типов. Это затруднит объединение терминов, не зная во время компиляции, какие типы у этих терминов.

Но если вы не возражаете против чего-то эквивалентного, которое выглядит совершенно иначе, хорошо известно, что комбинаторы SKI эквивалентны лямбда-исчислению. А поскольку SKI не предлагает явных лямбда-выражений или вообще ссылок на переменные, нет способа закодировать незамкнутый терм.

Answer 3

Конечно, это даже реализовано как связанная библиотека , которая является обобщением представления индексов Де Брёйна с использованием (полиморфно) рекурсивного типа данных:

      data Var bound free
  = Bound bound
  | Free free

newtype Scope bound term a
  = Scope { runScope :: term (Var bound (term a)) }

data Term var
  = Var var
  | App (Term var) (Term var)
  | Lam (Scope () Term var)
  -- == Lam (Term (Var () (Term var)))

Тип терминов индексируется типом переменных в этих терминах, как связанных, так и свободных. При определении новой вложенной области в лямбда-терме мы меняем этот тип: для связанных переменных мы просто добавляем еще один уровень вложенности, здесь аннотированный с помощью ()дать простые индексы Де Брёйна; для бесплатных переменных мы просто передаем тип, но также добавляем уровень вложенности с помощью Term. Вложенность на уровне типа отражает количество уровней Де Брёйна, к которым могут относиться индексы.

Сейчас Term Voidэто тип терма без свободных переменных; он все еще может иметь связанные переменные в силу того факта, что рекурсия полиморфна: Lam (Scope (Var (Bound ()))) :: Term Void представляет (λx. x).

Этот метод работает на простом Haskell 98 (то есть без GADT), хотя есть преимущества добавления некоторых причудливых типов, например, я регулярно использую их для типизированных AST и статических типов проверки типов. Эд Кметт дал хороший обзор дизайна boundв школе Haskell. В этом пространстве есть связанные библиотеки, такие как unbound и unbound-generics.