A single representation for both strongly and weakly typed terms

TypedAndUntyped.hs

{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
module TypedAndUntyped where

import Control.Monad
import Control.Monad.Identity

import Data.Type.Equality
import Data.Typeable

-- | Just for the parser at the end.
import Text.ParserCombinators.Parsec
import qualified Text.Parsec.Token as P
import qualified Text.Parsec.Language as L


-- | The fixpoint combinator.
data Fix1 (e :: (k -> *) -> (k -> *)) (t :: k) where
  Fix1 :: e (Fix1 e) t -> Fix1 e t

-- | The language syntax expressed as an indexed functor.
data ExprF (e :: * -> *) (t :: *) where
  NLit :: Int -> ExprF e Int
  Plus :: e Int -> e Int -> ExprF e Int

  BLit :: Bool -> ExprF e Bool
  If :: e Bool -> e a -> e a -> ExprF e a

type Expr = Fix1 ExprF

tInt :: Int -> Expr Int
tInt = Fix1 . NLit

tBool :: Bool -> Expr Bool
tBool = Fix1 . BLit

tPlus :: Expr Int -> Expr Int -> Expr Int
tPlus a b = Fix1 $ Plus a b

tIf :: Expr Bool -> Expr a -> Expr a -> Expr a
tIf i t e = Fix1 $ If i t e

-- * Natural Transformations (Included from [compdata](https://hackage.haskell.org/package/compdata))

type (:->) f g = forall a. f a -> g a

class HFunctor f where
  hfmap :: a :-> b -> f a :-> f b

instance HFunctor ExprF where
  hfmap _ (NLit n) = NLit n
  hfmap f (Plus a b) = Plus (f a) (f b)
  hfmap _ (BLit b) = BLit b
  hfmap f (If a b c) = If (f a) (f b) (f c)



-- * Evaluation/Interpretation

-- | Interpretation of the language functor.
evalF :: ExprF Identity t -> Identity t
evalF (NLit n)   = return n
evalF (Plus a b) = (+) <$> a <*> b
evalF (BLit b)   = return b
evalF (If i t e) = ite <$> i <*> t <*> e
  where ite i t e = if i then t else e

-- | Evaluate an entire expression.
evaluate :: Expr t -> t
evaluate = runIdentity . evaluate'
    where
      evaluate' :: Fix1 ExprF :-> Identity
      evaluate' (Fix1 e) = evalF $ hfmap evaluate' e


-- * Untyped Expressions

-- | The function that hides the type.
data IgnoreT (e :: (k -> *) -> (k -> *)) (u :: k -> *) (t :: k) where
  IgnoreT :: forall t' e u t. e u t' -> IgnoreT e u t


-- | Untyped expressions.
type UExpr = Fix1 (IgnoreT ExprF) ()

-- | Ignore types on a term.
untype :: ExprF (Fix1 (IgnoreT ExprF)) t -> UExpr
untype = Fix1 . IgnoreT

-- | Wrap an untyped expression to fit into any typed hole.
rewrap :: forall (t :: *). UExpr -> Fix1 (IgnoreT ExprF) t
rewrap (Fix1 (IgnoreT e)) = Fix1 (IgnoreT e)

uInt :: Int -> UExpr
uInt = untype . NLit

uBool :: Bool -> UExpr
uBool = untype . BLit

uPlus :: UExpr -> UExpr -> UExpr
uPlus l r = untype $ Plus (rewrap l) (rewrap r)

uIf :: UExpr -> UExpr -> UExpr -> UExpr
uIf i t e = untype $ If (rewrap i) t e



-- * Type Checking

-- | Existential quantification over `Typeable` types.
data Ex (f :: k -> *) where
  Ex :: forall t f. Typeable t => f t -> Ex f

-- | A pair of inference and checking functions.
data CheckInfer (m :: * -> *) (f :: k -> *) (t :: k) = CheckInfer
  { check :: forall t'. Typeable t' => m (f t')
  , infer :: m (Ex f)
  }

instance Functor m => HFunctor (CheckInfer m) where
  hfmap f CheckInfer{..} = CheckInfer
    { check = f <$> check
    , infer = exNT f <$> infer
    }
    where exNT :: f :-> g -> Ex f -> Ex g
          exNT f (Ex a) = Ex (f a)


-- | Build a @CheckInfer@ from just an `infer`.
fromInfer :: forall m f t. MonadPlus m => m (Ex f) -> CheckInfer m f t
fromInfer val = CheckInfer
  { check = do
      Ex e <- val
      check e
  , infer = val
  }
  where check :: forall t t'. (Typeable t, Typeable t') => f t' -> m (f t)
        check e = case eqT @t @t' of
                    Just Refl -> return e
                    Nothing -> mzero

-- | Type checking function for the language functor.
checkF :: MonadPlus m
       => IgnoreT ExprF (CheckInfer m e) t
       -> CheckInfer m (ExprF e) t
checkF (IgnoreT (NLit n)) =
  fromInfer $ return (Ex (NLit n))
checkF (IgnoreT (Plus a b)) =
  fromInfer $ (\ a b -> Ex (Plus a b)) <$> check a <*> check b
checkF (IgnoreT (BLit n)) = fromInfer $ return (Ex (BLit n))
checkF (IgnoreT (If i t e)) = CheckInfer
  { check = do
      it <- check i
      If it <$> check t <*> check e
  , infer = do
      it <- check i
      Ex tt <- infer t
      et <- check e
      return $ Ex (If it tt et)
  }


typeCheck' :: MonadPlus m => Fix1 (IgnoreT ExprF) :-> CheckInfer m (Fix1 ExprF)
typeCheck' (Fix1 (IgnoreT v)) =
  hfmap Fix1 $ checkF $ IgnoreT $ hfmap typeCheck' v

checkType :: (MonadPlus m, Typeable t) => UExpr -> m (Expr t)
checkType e = check $ typeCheck' e

inferType :: MonadPlus m => UExpr -> m (Ex Expr)
inferType e = infer $ typeCheck' e


-- * Parsing

parseExprF :: GenParser Char st UExpr
parseExprF =
      do string "(+ "
         l <- parseExprF
         string " "
         r <- parseExprF
         string ")"
         return $ uPlus l r
  <|> do string "(if"
         i <- parseExprF
         string " "
         t <- parseExprF
         string " "
         e <- parseExprF
         string ")"
         return $ uIf i t e
  <|> do string "true"
         return $ uBool True
  <|> do string "false"
         return $ uBool False
  <|> uInt . read <$> many1 digit

parseExpr :: GenParser Char st UExpr
parseExpr = do
  e <- parseExprF
  return e



showVal :: forall t. Typeable t => t -> String
showVal = case eqT @t @Int of
            Just Refl -> show @Int
            Nothing -> case eqT @t @Bool of
                         Just Refl -> show @Bool
                         Nothing -> const "<unknown>"


-- | Entry-point
main :: IO ()
main = do
  prg <- getContents
  case parse parseExpr "" prg of
    Left err -> putStrLn $ show err
    Right val -> case inferType val of
                   Nothing -> putStrLn "ill-typed"
                   Just (Ex e) -> do
                     let val = evaluate e
                     putStrLn $ showVal val



-- * Compositional Types

data (:+:) (l :: (k -> *) -> (k -> *)) r u t where
  InL :: l u t -> (:+:) l r u t
  InR :: r u t -> (:+:) l r u t

iso1 :: IgnoreT (f :+: g) u t -> (IgnoreT f :+: IgnoreT g) u t
iso1 (IgnoreT (InL f)) = InL (IgnoreT f)
iso1 (IgnoreT (InR f)) = InR (IgnoreT f)

iso2 :: (IgnoreT f :+: IgnoreT g) u t -> IgnoreT (f :+: g) u t
iso2 (InL (IgnoreT f)) = IgnoreT (InL f)
iso2 (InR (IgnoreT f)) = IgnoreT (InR f)