Copyright	Copyright (c) 2017 the Hakaru team
License	BSD3
Stability	experimental
Portability	GHC-only
Safe Haskell	None
Language	Haskell2010

Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad

Contents

Orphan instances

Description

Bidirectional type checking for our AST.

Synopsis

type Input = Maybe (Vector Text)
type Ctx = VarSet ('KProxy :: KProxy Hakaru)
data TypeCheckMode
- = StrictMode
- | LaxMode
- | UnsafeMode
type TypeCheckError = Text
newtype TypeCheckMonad a = TCM {
- unTCM :: Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
}
runTCM :: TypeCheckMonad a -> Input -> TypeCheckMode -> Either TypeCheckError a
getInput :: TypeCheckMonad Input
getMode :: TypeCheckMonad TypeCheckMode
pushCtx :: Variable (a :: Hakaru) -> TypeCheckMonad b -> TypeCheckMonad b
getCtx :: TypeCheckMonad Ctx
failwith :: TypeCheckError -> TypeCheckMonad r
failwith_ :: TypeCheckError -> TypeCheckMonad r
try :: TypeCheckMonad a -> TypeCheckMonad (Maybe a)
tryWith :: TypeCheckMode -> TypeCheckMonad a -> TypeCheckMonad (Maybe a)
makeErrMsg :: Text -> Maybe SourceSpan -> Text -> TypeCheckMonad TypeCheckError
typeMismatch :: Maybe SourceSpan -> Either Text (Sing (a :: Hakaru)) -> Either Text (Sing (b :: Hakaru)) -> TypeCheckMonad r
missingInstance :: Text -> Sing (a :: Hakaru) -> Maybe SourceSpan -> TypeCheckMonad r
missingLub :: Sing (a :: Hakaru) -> Sing (b :: Hakaru) -> Maybe SourceSpan -> TypeCheckMonad r
ambiguousFreeVariable :: Text -> Maybe SourceSpan -> TypeCheckMonad r
ambiguousNullCoercion :: Maybe SourceSpan -> TypeCheckMonad r
ambiguousEmptyNary :: Maybe SourceSpan -> TypeCheckMonad r
ambiguousMustCheckNary :: Maybe SourceSpan -> TypeCheckMonad r
ambiguousMustCheck :: Maybe SourceSpan -> TypeCheckMonad r
argumentNumberError :: TypeCheckMonad r
data TypedAST (abt :: [Hakaru] -> Hakaru -> *) = forall b. TypedAST !(Sing b) !(abt '[] b)
onTypedAST :: (forall b. abt '[] b -> abt '[] b) -> TypedAST abt -> TypedAST abt
onTypedASTM :: Functor m => (forall b. abt '[] b -> m (abt '[] b)) -> TypedAST abt -> m (TypedAST abt)
elimTypedAST :: (forall b. Sing b -> abt '[] b -> x) -> TypedAST abt -> x
data TypedASTs (abt :: [Hakaru] -> Hakaru -> *) = forall b. TypedASTs !(Sing b) [abt '[] b]
data TypedReducer (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru]) = forall b. TypedReducer !(Sing b) (List1 Variable xs) (Reducer abt xs b)
data SomePattern (a :: Hakaru) = forall vars. SP !(Pattern vars a) !(List1 Variable vars)
data SomePatternCode xss t = forall vars. SPC !(PDatumCode xss vars (HData' t)) !(List1 Variable vars)
data SomePatternStruct xs t = forall vars. SPS !(PDatumStruct xs vars (HData' t)) !(List1 Variable vars)
data SomePatternFun x t = forall vars. SPF !(PDatumFun x vars (HData' t)) !(List1 Variable vars)
data SomeBranch a abt = forall b. SomeBranch !(Sing b) [Branch a abt b]
makeVar :: forall (a :: Hakaru). Variable 'U -> Sing a -> Variable a
make_NaryOp :: Sing a -> NaryOp -> TypeCheckMonad (NaryOp a)
isBool :: Sing a -> TypeCheckMonad (TypeEq a HBool)
jmEq1_ :: Sing (a :: Hakaru) -> Sing (b :: Hakaru) -> TypeCheckMonad (TypeEq a b)
getHEq :: Sing a -> TypeCheckMonad (HEq a)
getHOrd :: Sing a -> TypeCheckMonad (HOrd a)
getHSemiring :: Sing a -> TypeCheckMonad (HSemiring a)
getHRing :: Sing a -> TypeCheckMode -> TypeCheckMonad (SomeRing a)
getHFractional :: Sing a -> TypeCheckMode -> TypeCheckMonad (SomeFractional a)
lc :: (LC_ abt a -> LC_ abt b) -> abt '[] a -> abt '[] b
coerceTo_nonLC :: ABT Term abt => Coercion a b -> abt xs a -> abt xs b
coerceFrom_nonLC :: ABT Term abt => Coercion a b -> abt xs b -> abt xs a

Documentation

type Input = Maybe (Vector Text) Source #

Definition of the typechecking monad and related types/functions/instances.

type Ctx = VarSet ('KProxy :: KProxy Hakaru) Source #

data TypeCheckMode Source #

Constructors

StrictMode
LaxMode
UnsafeMode

Instances

Instances details

Read TypeCheckMode Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad Methods readsPrec :: Int -> ReadS TypeCheckMode # readList :: ReadS [TypeCheckMode] # readPrec :: ReadPrec TypeCheckMode # readListPrec :: ReadPrec [TypeCheckMode] #
Show TypeCheckMode Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad Methods showsPrec :: Int -> TypeCheckMode -> ShowS # show :: TypeCheckMode -> String # showList :: [TypeCheckMode] -> ShowS #

type TypeCheckError = Text Source #

newtype TypeCheckMonad a Source #

Constructors

TCM
Fields unTCM :: Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a

Instances

Instances details

Monad TypeCheckMonad Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad Methods (>>=) :: TypeCheckMonad a -> (a -> TypeCheckMonad b) -> TypeCheckMonad b # (>>) :: TypeCheckMonad a -> TypeCheckMonad b -> TypeCheckMonad b # return :: a -> TypeCheckMonad a #
Functor TypeCheckMonad Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad Methods fmap :: (a -> b) -> TypeCheckMonad a -> TypeCheckMonad b # (<$) :: a -> TypeCheckMonad b -> TypeCheckMonad a #
MonadFail TypeCheckMonad Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad Methods fail :: String -> TypeCheckMonad a #
Applicative TypeCheckMonad Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad Methods pure :: a -> TypeCheckMonad a # (<>) :: TypeCheckMonad (a -> b) -> TypeCheckMonad a -> TypeCheckMonad b # liftA2 :: (a -> b -> c) -> TypeCheckMonad a -> TypeCheckMonad b -> TypeCheckMonad c # (>) :: TypeCheckMonad a -> TypeCheckMonad b -> TypeCheckMonad b # (<*) :: TypeCheckMonad a -> TypeCheckMonad b -> TypeCheckMonad a #

runTCM :: TypeCheckMonad a -> Input -> TypeCheckMode -> Either TypeCheckError a Source #

getInput :: TypeCheckMonad Input Source #

Return the mode in which we're checking/inferring types.

getMode :: TypeCheckMonad TypeCheckMode Source #

Return the mode in which we're checking/inferring types.

pushCtx :: Variable (a :: Hakaru) -> TypeCheckMonad b -> TypeCheckMonad b Source #

Extend the typing context, but only locally.

getCtx :: TypeCheckMonad Ctx Source #

failwith :: TypeCheckError -> TypeCheckMonad r Source #

failwith_ :: TypeCheckError -> TypeCheckMonad r Source #

try :: TypeCheckMonad a -> TypeCheckMonad (Maybe a) Source #

a la optional :: Alternative f => f a -> f (Maybe a) but without needing the empty of the Alternative class.

tryWith :: TypeCheckMode -> TypeCheckMonad a -> TypeCheckMonad (Maybe a) Source #

Tries to typecheck in a given mode

makeErrMsg :: Text -> Maybe SourceSpan -> Text -> TypeCheckMonad TypeCheckError Source #

Helpers for constructing error messages

typeMismatch :: Maybe SourceSpan -> Either Text (Sing (a :: Hakaru)) -> Either Text (Sing (b :: Hakaru)) -> TypeCheckMonad r Source #

Fail with a type-mismatch error.

missingInstance :: Text -> Sing (a :: Hakaru) -> Maybe SourceSpan -> TypeCheckMonad r Source #

missingLub :: Sing (a :: Hakaru) -> Sing (b :: Hakaru) -> Maybe SourceSpan -> TypeCheckMonad r Source #

ambiguousFreeVariable :: Text -> Maybe SourceSpan -> TypeCheckMonad r Source #

ambiguousNullCoercion :: Maybe SourceSpan -> TypeCheckMonad r Source #

ambiguousEmptyNary :: Maybe SourceSpan -> TypeCheckMonad r Source #

ambiguousMustCheckNary :: Maybe SourceSpan -> TypeCheckMonad r Source #

ambiguousMustCheck :: Maybe SourceSpan -> TypeCheckMonad r Source #

argumentNumberError :: TypeCheckMonad r Source #

data TypedAST (abt :: [Hakaru] -> Hakaru -> *) Source #

Terms whose type is existentially quantified packed with a singleton for the type.

The e' ∈ τ portion of the inference judgement.

Constructors

forall b. TypedAST !(Sing b) !(abt '[] b)

Instances

Instances details

Show2 abt => Show (TypedAST abt) Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad Methods showsPrec :: Int -> TypedAST abt -> ShowS # show :: TypedAST abt -> String # showList :: [TypedAST abt] -> ShowS #

onTypedAST :: (forall b. abt '[] b -> abt '[] b) -> TypedAST abt -> TypedAST abt Source #

onTypedASTM :: Functor m => (forall b. abt '[] b -> m (abt '[] b)) -> TypedAST abt -> m (TypedAST abt) Source #

elimTypedAST :: (forall b. Sing b -> abt '[] b -> x) -> TypedAST abt -> x Source #

data TypedASTs (abt :: [Hakaru] -> Hakaru -> *) Source #

Constructors

forall b. TypedASTs !(Sing b) [abt '[] b]

data TypedReducer (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru]) Source #

Constructors

forall b. TypedReducer !(Sing b) (List1 Variable xs) (Reducer abt xs b)

data SomePattern (a :: Hakaru) Source #

Constructors

forall vars. SP !(Pattern vars a) !(List1 Variable vars)

data SomePatternCode xss t Source #

Constructors

forall vars. SPC !(PDatumCode xss vars (HData' t)) !(List1 Variable vars)

data SomePatternStruct xs t Source #

Constructors

forall vars. SPS !(PDatumStruct xs vars (HData' t)) !(List1 Variable vars)

data SomePatternFun x t Source #

Constructors

forall vars. SPF !(PDatumFun x vars (HData' t)) !(List1 Variable vars)

data SomeBranch a abt Source #

Constructors

forall b. SomeBranch !(Sing b) [Branch a abt b]

makeVar :: forall (a :: Hakaru). Variable 'U -> Sing a -> Variable a Source #

Misc.

make_NaryOp :: Sing a -> NaryOp -> TypeCheckMonad (NaryOp a) Source #

isBool :: Sing a -> TypeCheckMonad (TypeEq a HBool) Source #

jmEq1_ :: Sing (a :: Hakaru) -> Sing (b :: Hakaru) -> TypeCheckMonad (TypeEq a b) Source #

getHEq :: Sing a -> TypeCheckMonad (HEq a) Source #

getHOrd :: Sing a -> TypeCheckMonad (HOrd a) Source #

getHSemiring :: Sing a -> TypeCheckMonad (HSemiring a) Source #

getHRing :: Sing a -> TypeCheckMode -> TypeCheckMonad (SomeRing a) Source #

getHFractional :: Sing a -> TypeCheckMode -> TypeCheckMonad (SomeFractional a) Source #

lc :: (LC_ abt a -> LC_ abt b) -> abt '[] a -> abt '[] b Source #

coerceTo_nonLC :: ABT Term abt => Coercion a b -> abt xs a -> abt xs b Source #

coerceFrom_nonLC :: ABT Term abt => Coercion a b -> abt xs b -> abt xs a Source #

Orphan instances

ABT Term abt => Coerce (Branch a abt) Source #
Instance details Methods coerceTo :: forall (a0 :: Hakaru) (b :: Hakaru). Coercion a0 b -> Branch a abt a0 -> Branch a abt b Source # coerceFrom :: forall (a0 :: Hakaru) (b :: Hakaru). Coercion a0 b -> Branch a abt b -> Branch a abt a0 Source #