More.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-# OPTIONS_GHC -Wno-unused-imports #-}
{-# OPTIONS_GHC -Wno-unused-matches #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

import Data.List (intercalate)
import Data.String (IsString, fromString)
import GHC.TypeLits (KnownSymbol, Symbol, someSymbolVal, symbolVal)


-- Singletons for built-in symbols. (Unused!)

-- data SingSymbol :: Symbol -> * where
--   SingKnownSymbol :: forall s. KnownSymbol s => SingSymbol s
--
-- unsingSymbol :: forall s. SingSymbol s -> String
-- unsingSymbol ss@SingKnownSymbol = symbolVal ss


-- Naturals.

data Nat :: * where
  Zero :: Nat
  Suc  :: Nat -> Nat

instance Eq Nat where
  Zero  == Zero   = True
  Suc n == Suc n' = n == n'
  _     == _      = False

instance Ord Nat where
  Zero  <= _      = True
  Suc n <= Suc n' = n <= n'
  _     <= _      = False

instance Enum Nat where
  fromEnum Zero        = 0
  fromEnum (Suc n)     = fromEnum n + 1
  toEnum n | n == 0    = Zero
           | n > 0     = Suc (toEnum (n - 1))
           | otherwise = error "Cannot cast negative Int to Nat"

instance Show Nat where
  show = show . fromEnum


-- Singletons for naturals.

data SingNat :: Nat -> * where
  SingZero :: SingNat Zero
  SingSuc  :: forall n. SingNat n -> SingNat (Suc n)
  
class IsNat (n :: Nat) where
  singNat :: SingNat n
  
instance IsNat Zero where
  singNat = SingZero
  
instance IsNat n => IsNat (Suc n) where
  singNat = SingSuc singNat


-- Types.

infixl 9 :&&
infixr 7 :=>
data Ty :: * where
  Atom  :: String -> Ty
  (:=>) :: Ty -> Ty -> Ty
  (:&&) :: Ty -> Ty -> Ty
  Top   :: Ty

instance Show Ty where
  show (Atom s)  = s
  show (a :=> b) = "(" ++ show a ++ " ⊃ " ++ show b ++ ")"
  show (a :&& b) = "(" ++ show a ++ " ∧ " ++ show b ++ ")"
  show Top       = "⊤"

instance IsString Ty where
  fromString = Atom . fromString
  
  
-- Singletons for types.

data SingTy :: Ty -> * where
  SingAtom :: forall s. SingTy (Atom s)
  SingImp  :: forall a b. SingTy a -> SingTy b -> SingTy (a :=> b)
  SingConj :: forall a b. SingTy a -> SingTy b -> SingTy (a :&& b)
  SingTop  :: SingTy Top

class IsTy (a :: Ty) where
  singTy :: SingTy a
  
instance forall s. IsTy (Atom s) where
  singTy = SingAtom

instance forall a b. (IsTy a, IsTy b) => IsTy (a :=> b) where
  singTy = SingImp singTy singTy
    
instance forall a b. (IsTy a, IsTy b) => IsTy (a :&& b) where
  singTy = SingConj singTy singTy
  
instance IsTy Top where
  singTy = SingTop
  
unsingTy :: forall a. SingTy a -> Ty
unsingTy SingAtom         = Atom _
unsingTy (SingImp sa sb)  = unsingTy sa :=> unsingTy sb
unsingTy (SingConj sa sb) = unsingTy sa :&& unsingTy sb
unsingTy SingTop          = Top


-- Contexts.

infixl 5 :.
data Cx :: * where
  Nil  :: Cx
  (:.) :: Cx -> Ty -> Cx

instance Show Cx where
  show cx = "{" ++ intercalate ", " (map show (fromList cx)) ++ "}"

fromList :: Cx -> [Ty]
fromList = reverse . helpFromList
  where
    helpFromList Nil       = []
    helpFromList (cx :. a) = a : fromList cx
    

-- Singletons for contexts.

data SingCx :: Cx -> * where
  SingNil  :: SingCx Nil
  SingSnoc :: forall cx a. SingCx cx -> SingTy a -> SingCx (cx :. a)
  
class IsCx (cx :: Cx) where
  singCx :: SingCx cx
  
instance IsCx Nil where
  singCx = SingNil
  
instance forall cx a. (IsCx cx, IsTy a) => IsCx (cx :. a) where
  singCx = SingSnoc singCx singTy
  
unsingCx :: forall cx. SingCx cx -> Cx
unsingCx SingNil           = Nil
unsingCx (SingSnoc scx sa) = unsingCx scx :. unsingTy sa


-- Context membership, or typed de Bruijn indices.

data In :: Cx -> Ty -> * where
  Here  :: In (cx :. a) a
  There :: In cx a -> In (cx :. b) a

instance forall cx a. Eq (In cx a) where
  Here    == Here     = True
  There i == There i' = i == i'
  _       == _        = False

instance forall cx a. Ord (In cx a) where
  Here    <= _        = True
  There i <= There i' = i <= i'
  _       <= _        = False

instance forall cx a. Enum (In cx a) where
  fromEnum Here      = 0
  fromEnum (There i) = fromEnum i + 1
  toEnum _           = error "Cannot cast Int to typed de Bruijn index"

instance forall cx a. Show (In cx a) where
  show i = "i" ++ show (fromEnum i)


-- Terms.

data Tm :: Cx -> Ty -> * where
  Var  :: forall cx a.   In cx a -> Tm cx a
  Lam  :: forall cx a b. Tm (cx :. a) b -> Tm cx (a :=> b)
  App  :: forall cx a b. Tm cx (a :=> b) -> Tm cx a -> Tm cx b
  Pair :: forall cx a b. Tm cx a -> Tm cx b -> Tm cx (a :&& b)
  Fst  :: forall cx a b. Tm cx (a :&& b) -> Tm cx a
  Snd  :: forall cx a b. Tm cx (a :&& b) -> Tm cx b
  Unit :: forall cx.     Tm cx Top

contextOf :: forall cx a. IsCx cx => Tm cx a -> SingCx cx
contextOf t = singCx

typeOf :: forall cx a. IsTy a => Tm cx a -> SingTy a
typeOf t = singTy

instance forall cx a. Show (Tm cx a) where
  show (Var i)    = "v" ++ show (fromEnum i)
  show (Lam t)    = "(lam " ++ show t ++ ")"
  show (App t u)  = "(app " ++ show t ++ " " ++ show u ++ ")"
  show (Pair t u) = "(pair " ++ show t ++ " " ++ show u ++ ")"
  show (Fst t)    = "(fst " ++ show t ++ ")"
  show (Snd t)    = "(snd " ++ show t ++ ")"
  show Unit       = "unit"