module Compiler.Typesystem.SimplyTyped where
import Calculi.Lambda
import Calculi.Lambda.Cube.SimpleType
import Control.Typecheckable
import Control.Monad
import qualified Control.Monad.State as State
import Data.Bifunctor
import Data.Generics
import qualified Data.Map as Map
import Data.Random.Generics
import Data.Semigroup
import qualified Data.Set as Set
import Test.QuickCheck
import qualified Language.Haskell.TH.Lift as TH
data SimplyTyped m =
Mono m
| Function (SimplyTyped m) (SimplyTyped m)
deriving (Show, Read, Eq, Ord, Data)
TH.deriveLift ''SimplyTyped
instance Functor SimplyTyped where
fmap f = \case
Mono m -> Mono (f m)
Function from to -> Function (fmap f from) (fmap f to)
instance Foldable SimplyTyped where
foldr f z = \case
Mono m -> f m z
Function from to -> foldr f (foldr f z to) from
instance Ord m => SimpleType (SimplyTyped m) where
type MonoType (SimplyTyped m) = m
abstract = Function
reify (Function from to) = Just (from, to)
reify _ = Nothing
bases (Mono m) = Set.singleton (Mono m)
bases (Function from to) = bases from `Set.union` bases to
mono = Mono
equivalent = (==)
data SimplyTypedErr c v t =
STNotKnownErr (NotKnownErr c v t)
| STSimpleTypeErr (SimpleTypeErr t)
deriving (Eq, Ord, Show)
instance (Ord m, Ord c, Ord v) => Typecheckable (LambdaTerm c v) (SimplyTyped m) where
type TypingContext (LambdaTerm c v) (SimplyTyped m) = (SimpleTypingContext c v (SimplyTyped m))
type TypeError (LambdaTerm c v) (SimplyTyped m) =
ErrorContext'
(LambdaTerm c v)
(SimplyTyped m) (SimplyTypedErr c v (SimplyTyped m))
typecheck env _expr =
first (fmap (\err -> err { _expression = _expr : _expression err }))
$ case _expr of
Variable v ->
let
err = Left [ErrorContext [] env (STNotKnownErr (UnknownVariable v))]
success = (Right . (,) env)
in maybe err success (Map.lookup v (_variables env))
(Apply fun arg) ->
let
fun' = typecheck env fun
arg' = typecheck env arg
in case (fun', arg') of
(Left fun'err, Left arg'err) -> Left $ fun'err <> arg'err
_ -> do
(_, fun'type) <- fun'
(_, arg'type) <- arg'
case reify fun'type of
Nothing ->
Left [ErrorContext [fun] env (STSimpleTypeErr $ NotAFunction fun'type)]
Just (funarg'type, funret'type)
| funarg'type /= arg'type ->
Left [ErrorContext [fun] env (STSimpleTypeErr $ UnexpectedType funarg'type arg'type)]
| otherwise ->
Right (env, funret'type)
(Lambda (var, var'type) expr) -> do
let unknownTypes = Set.toList $ Set.difference (bases var'type) (_allTypes env)
let errFun t = ErrorContext [] env (STNotKnownErr$ UnknownType t)
unless (null unknownTypes) . Left $ errFun <$> unknownTypes
let env' = env { _variables = Map.insert var var'type (_variables env) }
(_, expr'type) <- typecheck env' expr
return (env, var'type /-> expr'type)
instance (Data m, Arbitrary m) => Arbitrary (SimplyTyped m) where
arbitrary = sized $ generatorPWith [alias (\() -> arbitrary :: Gen m)]