LambdaCalculusTypeLevel.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}

import           Data.Kind
import           Data.List
import           Data.Singletons.Prelude
import qualified Data.Text               as Text
import           GHC.TypeLits

data Expr0 = Lam0 String Expr0 | Var0 String | App0 Expr0 Expr0
  deriving (Show)

-- rem :: String -> Expr -> Expr -> Expr
-- rem n e (Var n1) | n == n1 = e
-- rem n e (Lam s e1) | n /= s = Lam s (rem n e e1)
-- rem n e (App e1 e2) = App (rem n e e1) (rem n e e2)

-- А теперь изменения, как реализовать функцию rem для такого типа.
-- (Код с idris, может, можно перевести на haskell)

type family DeleteAll (x :: k) xs where
  DeleteAll x '[] = '[]
  DeleteAll x (x ': xs) = DeleteAll x xs
  DeleteAll x (y ': xs) = y ': DeleteAll x xs

data Expr :: [Symbol] -> Type where
  Var :: KnownSymbol n => Expr '[n]
  App :: Expr l1 -> Expr l2 -> Expr (l1 ++ l2)
  Lam :: KnownSymbol n => Proxy n -> Expr l -> Expr (DeleteAll n l)

showVar :: forall n . KnownSymbol n => Expr '[n] -> String
showVar _ = symbolVal (Proxy @n)

instance Show (Expr syms) where
  show e = case e of
    Var     -> showVar e
    App f x -> concat ["(", show f, " ", show x, ")"]
    Lam x f -> concat ["(\\", symbolVal x, " . ", show f, ")"]

showSig :: forall (syms :: [Symbol]) . SingI syms => Expr syms -> String
showSig e =
  concat
    $   show e
    :   " : "
    :   "["
    :   intersperse ", " (map Text.unpack $ demote @syms)
    ++  ["]"]

main :: IO ()
main = do
  putStrLn $ showSig $ Var @"a"
  putStrLn $ showSig $ App (Var @"a") (Var @"b")
  putStrLn $ showSig $ Lam (Proxy @"a") (Var @"b")
  putStrLn $
    showSig $
      Lam
        (Proxy @"x")
        (App (App (Var @"f") (Var @"x")) (App (Var @"g") (Var @"x")))