Pure Type System draft

puretypesystem.hs

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}
{-# LANGUAGE OverloadedStrings #-}

module Main where

import           Control.Applicative
import           Data.Attoparsec.Text as A
import           Data.Bifoldable
import           Data.Char
import           Data.Functor
import           Data.Kind
import           Data.Map             as M
import qualified Data.Text            as T

-- >>> main
-- (λ(f : Natural → ✷) → f 3) λ(x : Natural) → Boolean
-- = Boolean : ✷
main :: IO ()
main =
  let system
        -- "((\\f:PiT:*.Pix:T.T.\\T:*.\\x:T.(f T) x) (\\T:*.\\x:T.x)) Natural"
       = "(\\f:Natural->*.f 3) (\\x:Natural.Boolean)"
   in bitraverse_ putStrLn printSystem (parseOnly parsePTS system)

printSystem :: PTS -> IO ()
printSystem system =
  case typecheck M.empty (hierarchy Predicative) system of
    Right ok ->
      putStrLn
        (T.unpack
           (prettyPrint system <> "\n= " <> prettyPrint (normalize system) <>
            " : " <>
            prettyPrint ok))
    Left err -> putStrLn $ T.unpack err

type Name = T.Text

type Value = String

type Universe = Nat

type Index = Nat

data HierarchyType
  = Predicative
  | Impredicative

type Hierarchy = Universe -> Universe -> Universe

data Nat :: Type where
  Z :: Nat
  S :: Nat -> Nat
  deriving (Show, Eq, Ord)

data PureType :: Type where
  PTNat :: PureType
  PTBool :: PureType
  deriving (Show, Eq)

data PureLiteral :: Type where
  PLNat :: Nat -> PureLiteral
  PLBool :: Bool -> PureLiteral
  deriving (Show, Eq)

data PTS :: Type where
  Type :: PureType -> PTS
  Lit :: PureLiteral -> PTS
  Var :: Index -> Name -> PTS
  Star :: Universe -> PTS
  App :: PTS -> PTS -> PTS
  Lambda :: Name -> Universe -> PTS -> PTS -> PTS
  Pi :: Name -> Universe -> PTS -> PTS -> PTS
  deriving (Show)

natToInt :: Nat -> Int
natToInt Z     = 0
natToInt (S k) = 1 + natToInt k

intToNat :: Int -> Nat
intToNat 0 = Z
intToNat x = S $ intToNat $ x - 1

prettyPrint :: PTS -> Name
prettyPrint (Lit (PLNat n)) = T.pack . show $ natToInt n
prettyPrint (Lit (PLBool b)) = T.pack . show $ b
prettyPrint (Type PTNat) = "Natural"
prettyPrint (Type PTBool) = "Boolean"
prettyPrint (Var _ n) = n
prettyPrint (Star Z) = "Term"
prettyPrint (Star (S Z)) = "✷"
prettyPrint (Star (S (S Z))) = "☐"
prettyPrint (Star (S (S k))) = "☐" <> T.replicate (natToInt k) "↑"
prettyPrint (App l@Lambda {} a) = "(" <> prettyPrint l <> ") " <> prettyPrint a
prettyPrint (App app@App {} a) = "(" <> prettyPrint app <> ") " <> prettyPrint a
prettyPrint (App f a) = prettyPrint f <> " " <> prettyPrint a
prettyPrint (Lambda n _ l r) =
  "λ(" <> n <> " : " <> prettyPrint l <> ")" <> " → " <> prettyPrint r
prettyPrint (Pi "_" _ l r) = prettyPrint l <> " → " <> prettyPrint r
prettyPrint (Pi n _ l r) =
  "Π(" <> n <> " : " <> prettyPrint l <> ")" <> " → " <> prettyPrint r

shift :: Name -> Index -> PTS -> PTS
shift n' i' v@(Var i n)
  | n == n' && i >= i' = Var (S i) n
  | otherwise = v
shift n' i' (Pi n u l r)
  | n == n' && u == Z = Pi n u (shift n' i' l) (shift n' (S i') r)
  | otherwise = Pi n u (shift n' i' l) (shift n' i' r)
shift n' i' (Lambda n u l r)
  | n == n' && u == Z = Lambda n u (shift n' i' l) (shift n' (S i') r)
  | otherwise = Lambda n u (shift n' i' l) (shift n' i' r)
shift _ _ x = x

substitute :: Name -> Index -> PTS -> PTS -> PTS
substitute n' i' v' v@(Var i n)
  | n == n' && i == i' = v'
  | n == n' && i > i' =
    let (Var (S k) _) = v
     in Var k n
  | otherwise = v
substitute n' i' v' (Pi n u l r)
  | n == n' && u == Z =
    Pi n Z (substitute n' i' v' l) (substitute n' (S i') (shift n' Z v') r)
  | otherwise =
    Pi n u (substitute n' i' v' l) (substitute n' i' (shift n Z v') r)
substitute n' i' v' (Lambda n u l r)
  | n == n' && u == Z =
    Lambda n Z (substitute n' i' v' l) (substitute n' (S i') (shift n' Z v') r)
  | otherwise =
    Lambda n u (substitute n' i' v' l) (substitute n' i' (shift n Z v') r)
substitute n' i' v' (App f a) =
  App (substitute n' i' v' f) (substitute n' i' v' a)
substitute _ _ _ x = x

normalize :: PTS -> PTS
normalize (Pi n Z l r) = Pi n Z (normalize l) (normalize r)
normalize (Lambda n Z l r) = Lambda n Z (normalize l) (normalize r)
normalize (App f a) =
  case normalize f of
    (Lambda n Z _ r) -> normalize $ substitute n Z a r
    normalForm       -> App normalForm (normalize a)
normalize x = x

equality :: PTS -> PTS -> Bool
equality (Pi n Z l r) (Pi n' Z l' r') =
  equality l l' && equality r (substitute n' Z (Var Z n) (shift n Z r'))
equality (Lambda n Z l r) (Lambda n' Z l' r') =
  equality l l' && equality r (substitute n' Z (Var Z n) (shift n Z r'))
equality (App f a) (App f' a') = equality f f' && equality a a'
equality (Var i n) (Var i' n') = i == i' && n == n'
equality (Star u) (Star u') = u == u'
equality (Lit x) (Lit x') = x == x'
equality (Type x) (Type x') = x == x'
equality _ _ = False

hierarchy :: HierarchyType -> Hierarchy
hierarchy Predicative x y   = max x y
hierarchy Impredicative _ y = y

typecheck :: M.Map (Name, Index) PTS -> Hierarchy -> PTS -> Either T.Text PTS
typecheck _ _ (Lit (PLNat _)) = pure $ Type PTNat
typecheck _ _ (Lit (PLBool _)) = pure $ Type PTBool
typecheck _ _ (Type _) = pure $ Star $ S Z
typecheck _ _ (Star x) = pure $ Star $ S x
typecheck e _ (Var i n)
  | M.member (n, i) e = pure $ e M.! (n, i)
  | otherwise =
    Left $
    "Variable " <> n <> "@" <> (T.pack . show) (natToInt i) <> " not found in " <>
    (T.pack . show) e
typecheck e h (Pi n Z l r) = do
  l' <- typecheck e h l
  r' <- typecheck (M.insert (n, Z) (normalize l) e) h r
  case (l', r') of
    (Star y, Star z) -> pure (Star $ h y z)
    _ ->
      Left $
      "Invalid Pi: " <> (T.pack . show) l <> " | " <> (T.pack . show) r <> ", " <>
      (T.pack . show) l' <>
      " | " <>
      (T.pack . show) r'
typecheck e h (Lambda n Z l r) = do
  l' <- typecheck e h l
  let lnorm = normalize l
  case l' of
    (Star _) -> do
      r' <- typecheck (M.insert (n, Z) lnorm e) h r
      pure $ Pi n Z lnorm r'
    _ ->
      Left $
      "Invalid Lambda: " <> (T.pack . show) l <> " | " <> (T.pack . show) l'
typecheck e h (App f a) = do
  f' <- typecheck e h f
  case f' of
    (Pi n Z l r) -> do
      a' <- typecheck e h a
      if equality l a'
        then pure $ normalize $ substitute n Z a r
        else Left $
             "Invalid rhs:\n>" <> (T.pack . show) l <> "=" <> (T.pack . show) a <>
             "\n>" <>
             (T.pack . show) l <>
             "=" <>
             (T.pack . show) a'
    _ ->
      Left $
      "Invalid App: { " <> (T.pack . show) f <> " " <> (T.pack . show) f' <>
      " | " <>
      (T.pack . show) a
typecheck _ _ x = Left $ "Invalid expression: " <> (T.pack . show) x

parsePTS :: Parser PTS
parsePTS =
  parseApp <|> ("(" *> parsePTS <* ")") <|> parseLambda <|> parsePI <|>
  parseType <|>
  parseLit <|>
  parseVar <|>
  parseStar

parseSubPTS :: Parser PTS
parseSubPTS =
  ("(" *> parsePTS <* ")") <|> parseType <|> parseLit <|> parseVar <|> parseStar

parseType :: Parser PTS
parseType = "Natural" $> Type PTNat <|> "Boolean" $> Type PTBool

parseLit :: Parser PTS
parseLit =
  Lit . PLNat . intToNat <$> decimal <|>
  Lit . PLBool <$> ("True" $> True <|> "False" $> False)

parseIdentifier :: Parser T.Text
parseIdentifier = A.takeWhile1 isAlpha

parseStar :: Parser PTS
parseStar = Star . intToNat . T.length <$> takeWhile1 (== '*')

parseLambda :: Parser PTS
parseLambda =
  "\\" *>
  (Lambda <$> parseIdentifier <*> pure Z <*> (":" *> parsePTS <* ".") <*>
   parsePTS)

parsePI :: Parser PTS
parsePI =
  ("Pi" *>
   (Pi <$> parseIdentifier <*> pure Z <*> (":" *> parsePTS <* ".") <*> parsePTS)) <|>
  (Pi "_" <$> pure Z <*> (parseSubPTS <* "->") <*> parseSubPTS)

parseApp :: Parser PTS
parseApp = App <$> parseSubPTS <*> (" " *> parsePTS)

parseVar :: Parser PTS
parseVar = Var Z <$> parseIdentifier