Validate.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

module Validate where

import Parse (Identifier)
import qualified Parse as Parsed
import Control.Monad.Error.Class (throwError)
import Data.Type.Equality ((:~:) (..))


newtype TypeError = TypeError String deriving Show

data Index env t where
  Zero :: Index (t : env) t
  Succ :: Index env t -> Index (t' : env) t

data Expression env t where
  BooleanLiteral :: Bool -> Expression env Bool
  IntegerLiteral :: Integer -> Expression env Integer
  Abstraction    :: Expression (t : env) t' -> Expression env (t -> t')
  Application    :: Expression env (t -> t') -> Expression env t -> Expression env t'
  Variable       :: Index env t -> Expression env t

data Any x = forall t. Some (x t)
infix  2 :::
data Annotated a = forall t. a t ::: Type t

infixr 3 :->:
data Type t where
  Boolean :: Type Bool
  Integer :: Type Integer
  (:->:)  :: Type a -> Type b -> Type (a -> b)

data TypeEnvironment env where
  Empty :: TypeEnvironment '[]
  Cons  :: (Identifier, Type t) -> TypeEnvironment env -> TypeEnvironment (t : env)


validate :: Parsed.Expression -> Either TypeError (Any (Expression '[]))
validate expr = go Empty expr >>= (\(expr ::: _) -> return $ Some expr)
  where
    go :: TypeEnvironment env -> Parsed.Expression -> Either TypeError (Annotated (Expression env))
    go env = \case
      Parsed.BooleanLiteral b -> return $ BooleanLiteral b ::: Boolean
      Parsed.IntegerLiteral i -> return $ IntegerLiteral i ::: Integer
      Parsed.Abstraction ident annot expr | Some paramType <- annotationToType annot -> do
        validExpr ::: returnType <- go (Cons (ident, paramType) env) expr
        return $ Abstraction validExpr ::: paramType :->: returnType
      Parsed.Application fun arg -> do
        fun' ::: funType <- go env fun
        arg' ::: argType <- go env arg
        case funType of
          paramType :->: returnType -> case compareTypes paramType argType of
            Just Refl -> return $ Application fun' arg' ::: returnType
            _         -> throwError $ TypeError "Incompatible argument type"
          _ -> throwError $ TypeError "Callee is not a function"
      Parsed.Variable ident -> do
        idx ::: typ <- resolve ident env
        return $ Variable idx ::: typ

    annotationToType :: Parsed.TypeExpression -> Any Type
    annotationToType = \case
      Parsed.Boolean  -> Some Boolean
      Parsed.Integer  -> Some Integer
      a Parsed.:->: b | Some a' <- annotationToType a
                      , Some b' <- annotationToType b
                      -> Some $ a' :->: b'
    
    compareTypes :: Type t -> Type t' -> Maybe (t :~: t')
    compareTypes Boolean    Boolean      = Just Refl
    compareTypes Integer    Integer      = Just Refl
    compareTypes (a :->: b) (a' :->: b') | Just Refl <- compareTypes a a'
                                         , Just Refl <- compareTypes b b'
                                         = Just Refl
    compareTypes _          _            = Nothing
    
    resolve :: Identifier -> TypeEnvironment env -> Either TypeError (Annotated (Index env))
    resolve ident Empty = throwError $ TypeError $ "Variable '" ++ ident ++ "' not in scope"
    resolve ident (Cons (ident', typ) env)
      | ident == ident' = return $ Zero ::: typ
      | otherwise       = do
      idx ::: typ <- resolve ident env
      return $ Succ idx ::: typ