The Calculus of Constructions.

Other.hs

-- https://gist.github.com/ChristopherKing42/d8c9fde0869ec5c8feae71714e069214
-- https://github.com/MaiaVictor/Cedille-Core/blob/master/old_haskell_implementation/Core.hs
-- https://crypto.stanford.edu/~blynn/lambda/pts.html

module Other where

import Prelude hiding (pi, succ)

import Control.Monad.Reader

import Data.Maybe (fromJust)

import Text.Parsec hiding (parse)

type Name = String

data Expr
  = Var Name
  | Lam Name Expr Expr
  | Pi Name Expr Expr
  | App Expr Expr
  | Type -- Star
  | Kind -- Box
  deriving (Eq, Show)

subst :: Name -> Expr -> Expr -> Expr
subst v e (Var v')
  | v == v' = e
subst v e (Lam v' ta b)
  | v == v'   = Lam v' (subst v e ta) b
  | otherwise = Lam v' (subst v e ta) (subst v e b)
subst v e (Pi v' ta tb)
  | v == v'   = Pi v' (subst v e ta) tb
  | otherwise = Pi v' (subst v e ta) (subst v e tb)
subst v e (App f a) = App (subst v e f) (subst v e a)
subst _ _ e = e

free :: Name -> Expr -> Bool
free v e = e /= subst v (Var "") e

toString :: Expr -> String
toString = go
  where
  go (Var v) = v
  go (Lam v ta b) = unwords ["λ", v, ":", parens ta, ",", go b]
  go (Pi v ta tb)
    | free v tb = unwords ["∀", v, ":", go ta, ",", go tb]
    | otherwise = unwords [parens ta, "→", go tb]
  go (App f a) = unwords [go f, parens a]
  go Type = "★"
  go Kind = "☐"

  parens (Var v) = v
  parens Type = "★"
  parens Kind = "☐"
  parens e = concat ["(", go e, ")"]

normalize :: Expr -> Expr
normalize (Lam v ta b) =
  case normalize b of
    App f (Var v') | v == v' && not (free v f) -> f -- Eta reduction
    b -> Lam v (normalize ta) b
normalize (Pi v ta tb) = Pi v (normalize ta) (normalize tb)
normalize (App f a) =
  case normalize f of
    Lam v _ b -> subst v (normalize a) b
    f -> App f (normalize a)
normalize e = e

equiv :: Expr -> Expr -> Bool
equiv e1 e2 = go 0 (normalize e1) (normalize e2)
  where
  go n (Lam v1 ta1 b1) (Lam v2 ta2 b2) = let
    b1' = subst v1 (Var (show n)) b1
    b2' = subst v2 (Var (show n)) b2
    in go n ta1 ta2 && go (n + 1) b1' b2'
  go n (Pi v1 ta1 tb1) (Pi v2 ta2 tb2) = let
    tb1' = subst v1 (Var (show n)) tb1
    tb2' = subst v2 (Var (show n)) tb2
    in go n ta1 ta2 && go (n + 1) tb1' tb2'
  go n (App f1 a1) (App f2 a2) = go n f1 f2 && go n a1 a2
  go _ e1 e2 = e1 == e2

typeOf :: Expr -> Maybe Expr
typeOf = go []
  where
  go ctx (Var v) = lookup v ctx
  go ctx (Lam v ta b) = do
    tb <- go ((v, ta) : ctx) b
    let t = Pi v ta tb
    _ <- go ctx t
    return t
  go ctx (Pi v ta tb) = do
    tb <- go ((v, ta) : ctx) tb
    ta <- go ctx ta
    case (ta, tb) of
      (Type, Type) -> return Type -- Simply Typed Lambda Calculus
      (Kind, Type) -> return Type -- System F
      (Type, Kind) -> return Kind -- Logical Framework
      (Kind, Kind) -> return Kind -- Type Operators
      _ -> Nothing
  go ctx (App f a) = do
    Pi v ta tb <- go ctx f
    ta' <- go ctx a
    if ta `equiv` ta'
      then return $ subst v a tb
      else Nothing
  go _ Type = return Kind
  go _ Kind = Nothing

-- Parser

type Parser = ParsecT String () (Reader [String])

parse :: String -> Maybe Expr
parse s =
  case runReader (runParserT (spaces *> expression <* eof) () "" s) [] of
    Left e -> error $ show e
    Right x -> Just x

isReserved :: Name -> Bool
isReserved x = elem x ["forall", "pi", "Π", "λ"]

expression :: Parser Expr
expression = pi
         <|> lambda
         <|> arrow

pi :: Parser Expr
pi = do
  try $ choice
    [ reserved "forall"
    , reserved "pi"
    , operator "Π"
    , operator "∀"
    ] *> spaces
  v <- name
  char ':' *> spaces
  ta <- expression
  char '.' *> spaces
  b <- local (v:) expression
  return $ Pi v ta b

lambda :: Parser Expr
lambda = do
  try $ operator "\\" <|> operator "λ"
  v <- name
  char ':' *> spaces
  ta <- expression
  char '.' *> spaces
  b <- local (v:) expression
  return $ Lam v ta b

arrow :: Parser Expr
arrow =
  application `chainr1` ((operator "->" <|> operator "→") *> return (Pi ""))

application :: Parser Expr
application = (star <|> variable <|> parens expression) `chainl1` return App

star :: Parser Expr
star = (operator "*" <|> operator "★") *> return Type

variable :: Parser Expr
variable = do
  v <- name
  env <- ask
  if elem v env
    then return $ Var v
    else fail $ "Unbound variable: " ++ v

name :: Parser String
name = do
  c <- letter
  cs <- many alphaNum
  spaces
  let s = c:cs
  if isReserved s
    then unexpected s
    else return s

reserved :: String -> Parser ()
reserved s = string s *> notFollowedBy alphaNum *> spaces

operator :: String -> Parser ()
operator s = string s *> spaces

parens :: Parser a -> Parser a
parens p = between open close p
  where
  open  = char '(' <* spaces
  close = char ')' <* spaces

-- Tests

s :: Expr
s = fromJust $ parse "λ a : * . λ b : * . λ c : * . λ x : (a → b → c) . λ y : (a → b) . λ z : a . x z (y z)"

k :: Expr
k = fromJust $ parse "λ a : * . λ b : * . λ x : a . λ y : b . x"

i :: Expr
i = fromJust $ parse "λ a : * . λ x : a . x"

nat :: Expr
nat = fromJust $ parse "∀ a : * . (a → a) → a → a"

zero :: Expr
zero = fromJust $ parse "λ a : * . λ s : (a → a) . λ z : a . z"

succ :: Expr
succ = fromJust $ parse "λ n : (∀ a : * . (a → a) → a → a) . λ a : * . λ s : (a → a) . λ z : a . s (n a s z)"

add :: Expr
add = fromJust $ parse "λ n : (∀ a : * . (a → a) → a → a) . λ m : (∀ a : * . (a → a) → a → a) . n (∀ a : * . (a → a) → a → a) (λ n : (∀ a : * . (a → a) → a → a) . λ a : * . λ s : (a → a) . λ z : a . s (n a s z)) m"

eq :: Expr
eq = fromJust $ parse "λ a : * . λ x : a . λ y : a . ∀ P : (a → *) . (P x) → P y"

-- putStrLn $ unlines $ map toString [s, k, i, nat, zero, succ, add, eq]
-- putStrLn $ unlines $ map (toString . fromJust . typeOf) [s, k, i, nat, zero, succ, add, eq]