Safe Haskell	None
Language	Haskell2010

Compiler.Typesystem.SystemF

Synopsis

Documentation

data SystemF m p Source #

An implementation of System-F, similar to haskell's own typesystems but without type-level functions beyond (→)

Constructors

Mono m
Poly p
Function (SystemF m p) (SystemF m p)
Forall p (SystemF m p)

Instances

Bifunctor SystemF Source #
Methods bimap :: (a -> b) -> (c -> d) -> SystemF a c -> SystemF b d # first :: (a -> b) -> SystemF a c -> SystemF b c # second :: (b -> c) -> SystemF a b -> SystemF a c #
Bitraversable SystemF Source #
Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> SystemF a b -> f (SystemF c d) #
Bifoldable SystemF Source #
Methods bifold :: Monoid m => SystemF m m -> m # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> SystemF a b -> m # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> SystemF a b -> c # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> SystemF a b -> c #
(Eq m, Eq p) => Eq (SystemF m p) Source #
Methods (==) :: SystemF m p -> SystemF m p -> Bool # (/=) :: SystemF m p -> SystemF m p -> Bool #
(Data m, Data p) => Data (SystemF m p) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SystemF m p -> c (SystemF m p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SystemF m p) # toConstr :: SystemF m p -> Constr # dataTypeOf :: SystemF m p -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (SystemF m p)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SystemF m p)) # gmapT :: (forall b. Data b => b -> b) -> SystemF m p -> SystemF m p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SystemF m p -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SystemF m p -> r # gmapQ :: (forall d. Data d => d -> u) -> SystemF m p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SystemF m p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SystemF m p -> m (SystemF m p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemF m p -> m (SystemF m p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemF m p -> m (SystemF m p) #
(Ord m, Ord p) => Ord (SystemF m p) Source #
Methods compare :: SystemF m p -> SystemF m p -> Ordering # (<) :: SystemF m p -> SystemF m p -> Bool # (<=) :: SystemF m p -> SystemF m p -> Bool # (>) :: SystemF m p -> SystemF m p -> Bool # (>=) :: SystemF m p -> SystemF m p -> Bool # max :: SystemF m p -> SystemF m p -> SystemF m p # min :: SystemF m p -> SystemF m p -> SystemF m p #
(Ord m, Ord p, Show m, Show p) => Show (SystemF m p) Source #
Methods showsPrec :: Int -> SystemF m p -> ShowS # show :: SystemF m p -> String # showList :: [SystemF m p] -> ShowS #
(Lift m0, Lift p0) => Lift (SystemF m0 p0) Source #
Methods lift :: SystemF m0 p0 -> Q Exp #
(Ord m, Ord p, Arbitrary m, Data m, Arbitrary p, Data p) => Arbitrary (SystemF m p) Source #
Methods arbitrary :: Gen (SystemF m p) # shrink :: SystemF m p -> [SystemF m p] #
(Ord m, Ord p) => SimpleType (SystemF m p) Source #
Associated Types type MonoType (SystemF m p) :: * Source # Methods abstract :: SystemF m p -> SystemF m p -> SystemF m p Source # reify :: SystemF m p -> Maybe (SystemF m p, SystemF m p) Source # bases :: SystemF m p -> Set (SystemF m p) Source # mono :: MonoType (SystemF m p) -> SystemF m p Source # equivalent :: SystemF m p -> SystemF m p -> Bool Source #
(Ord m, Ord p) => Polymorphic (SystemF m p) Source #
Associated Types type PolyType (SystemF m p) :: * Source # Methods substitutions :: SystemF m p -> SystemF m p -> Either [(SystemF m p, SystemF m p)] [Substitution (SystemF m p) (PolyType (SystemF m p))] Source # applySubstitution :: SystemF m p -> PolyType (SystemF m p) -> SystemF m p -> SystemF m p Source # quantify :: PolyType (SystemF m p) -> SystemF m p -> SystemF m p Source # poly :: PolyType (SystemF m p) -> SystemF m p Source # polytypesOf :: SystemF m p -> Set (SystemF m p) Source # quantifiedOf :: SystemF m p -> Set (SystemF m p) Source #
(Ord c, Ord v, Ord m, Ord p) => Typecheckable (LambdaTerm c v) (SystemF m p) Source #
Associated Types type TypingContext (LambdaTerm c v :: * -> ) (SystemF m p) :: Source # type TypeError (LambdaTerm c v :: * -> ) (SystemF m p) :: Source # Methods typecheck :: TypingContext (LambdaTerm c v) (SystemF m p) -> LambdaTerm c v (SystemF m p) -> Either [TypeError (LambdaTerm c v) (SystemF m p)] (TypingContext (LambdaTerm c v) (SystemF m p), SystemF m p) Source #
type MonoType (SystemF m p) Source #
type MonoType (SystemF m p) = m
type PolyType (SystemF m p) Source #
type PolyType (SystemF m p) = p
type TypingContext (LambdaTerm c v) (SystemF m p) Source #
type TypingContext (LambdaTerm c v) (SystemF m p) = SystemFContext c v (SystemF m p) p
type TypeError (LambdaTerm c v) (SystemF m p) Source #
type TypeError (LambdaTerm c v) (SystemF m p) = ErrorContext' (LambdaTerm c v) (SystemF m p) (SystemFErr c v (SystemF m p))

data SystemFErr c v t Source #

Error sum not within Eithers because those (GHC) type errors are messy.

Constructors

SFNotKnownErr (NotKnownErr c v t)
SFSimpleTypeErr (SimpleTypeErr t)
SFSubsErr (SubsErr Gr t (PolyType t))

Instances

(Polymorphic t, Eq v, Eq c) => Eq (SystemFErr c v t) Source #
Methods (==) :: SystemFErr c v t -> SystemFErr c v t -> Bool # (/=) :: SystemFErr c v t -> SystemFErr c v t -> Bool #
(Polymorphic t, Show v, Show c, Show t, Show (PolyType t)) => Show (SystemFErr c v t) Source #
Methods showsPrec :: Int -> SystemFErr c v t -> ShowS # show :: SystemFErr c v t -> String # showList :: [SystemFErr c v t] -> ShowS #

data SystemFContext c v t p Source #

Constructors

SystemFContext
Fields _polyctx :: SubsContext t p The context for Polymorphic related information _stlcctx :: SimpleTypingContext c v t The context for Simply-typed related information.

Instances

(Eq c, Eq v, Eq t, Eq p) => Eq (SystemFContext c v t p) Source #
Methods (==) :: SystemFContext c v t p -> SystemFContext c v t p -> Bool # (/=) :: SystemFContext c v t p -> SystemFContext c v t p -> Bool #
(Ord c, Ord v, Ord t, Ord p) => Ord (SystemFContext c v t p) Source #
Methods compare :: SystemFContext c v t p -> SystemFContext c v t p -> Ordering # (<) :: SystemFContext c v t p -> SystemFContext c v t p -> Bool # (<=) :: SystemFContext c v t p -> SystemFContext c v t p -> Bool # (>) :: SystemFContext c v t p -> SystemFContext c v t p -> Bool # (>=) :: SystemFContext c v t p -> SystemFContext c v t p -> Bool # max :: SystemFContext c v t p -> SystemFContext c v t p -> SystemFContext c v t p # min :: SystemFContext c v t p -> SystemFContext c v t p -> SystemFContext c v t p #
(Show c, Show v, Show t, Show p) => Show (SystemFContext c v t p) Source #
Methods showsPrec :: Int -> SystemFContext c v t p -> ShowS # show :: SystemFContext c v t p -> String # showList :: [SystemFContext c v t p] -> ShowS #

stlcctx :: forall c v t p c v. Lens (SystemFContext c v t p) (SystemFContext c v t p) (SimpleTypingContext c v t) (SimpleTypingContext c v t) Source #

polyctx :: forall c v t p p. Lens (SystemFContext c v t p) (SystemFContext c v t p) (SubsContext t p) (SubsContext t p) Source #