Compiler.Typesystem.SystemFOmega

System Fω is a System F that allows type operators (Set Int, List Int, Either Int Bool etc.)

Documentation

data SystemFOmega m p k

A data type representing the components of System-Fω, with a parameterized higher-order typesystem k.

Instances

Bifunctor (SystemFOmega m0)

Methods

bimap :: (a -> b) -> (c -> d) -> SystemFOmega m0 a c -> SystemFOmega m0 b d

first :: (a -> b) -> SystemFOmega m0 a c -> SystemFOmega m0 b c

second :: (b -> c) -> SystemFOmega m0 a b -> SystemFOmega m0 a c

Bitraversable (SystemFOmega m0)

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> SystemFOmega m0 a b -> f (SystemFOmega m0 c d)

Bifoldable (SystemFOmega m0)

Methods

bifold :: Monoid m => SystemFOmega m0 m m -> m

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> SystemFOmega m0 a b -> m

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> SystemFOmega m0 a b -> c

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> SystemFOmega m0 a b -> c

(Eq m, Eq p, Eq k) => Eq (SystemFOmega m p k)

Methods

(==) :: SystemFOmega m p k -> SystemFOmega m p k -> Bool

(/=) :: SystemFOmega m p k -> SystemFOmega m p k -> Bool

(Data m, Data p, Data k) => Data (SystemFOmega m p k)

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SystemFOmega m p k -> c (SystemFOmega m p k)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SystemFOmega m p k)

toConstr :: SystemFOmega m p k -> Constr

dataTypeOf :: SystemFOmega m p k -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (SystemFOmega m p k))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SystemFOmega m p k))

gmapT :: (forall b. Data b => b -> b) -> SystemFOmega m p k -> SystemFOmega m p k

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SystemFOmega m p k -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SystemFOmega m p k -> r

gmapQ :: (forall d. Data d => d -> u) -> SystemFOmega m p k -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SystemFOmega m p k -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SystemFOmega m p k -> m (SystemFOmega m p k)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemFOmega m p k -> m (SystemFOmega m p k)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemFOmega m p k -> m (SystemFOmega m p k)

(Ord m, Ord p, Ord k) => Ord (SystemFOmega m p k)

Methods

compare :: SystemFOmega m p k -> SystemFOmega m p k -> Ordering

(<) :: SystemFOmega m p k -> SystemFOmega m p k -> Bool

(<=) :: SystemFOmega m p k -> SystemFOmega m p k -> Bool

(>) :: SystemFOmega m p k -> SystemFOmega m p k -> Bool

(>=) :: SystemFOmega m p k -> SystemFOmega m p k -> Bool

max :: SystemFOmega m p k -> SystemFOmega m p k -> SystemFOmega m p k

min :: SystemFOmega m p k -> SystemFOmega m p k -> SystemFOmega m p k

(Read m, Read p, Read k) => Read (SystemFOmega m p k)

Methods

readsPrec :: Int -> ReadS (SystemFOmega m p k)

readList :: ReadS [SystemFOmega m p k]

readPrec :: ReadPrec (SystemFOmega m p k)

readListPrec :: ReadPrec [SystemFOmega m p k]

(Show m, Show p, Show k) => Show (SystemFOmega m p k)

Methods

showsPrec :: Int -> SystemFOmega m p k -> ShowS

show :: SystemFOmega m p k -> String

showList :: [SystemFOmega m p k] -> ShowS

(Lift m0, Lift p0, Lift k0) => Lift (SystemFOmega m0 p0 k0)

Methods

lift :: SystemFOmega m0 p0 k0 -> Q Exp

(Data m, Data p, Data k, Arbitrary m, Arbitrary p, Arbitrary k) => Arbitrary (SystemFOmega m p k)

Methods

arbitrary :: Gen (SystemFOmega m p k)

shrink :: SystemFOmega m p k -> [SystemFOmega m p k]

(Ord m, Ord p, Ord k) => SimpleType (SystemFOmega m p (Maybe k))

Associated Types

type MonoType (SystemFOmega m p (Maybe k)) :: *

Methods

abstract :: SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k)

reify :: SystemFOmega m p (Maybe k) -> Maybe (SystemFOmega m p (Maybe k), SystemFOmega m p (Maybe k))

bases :: SystemFOmega m p (Maybe k) -> Set (SystemFOmega m p (Maybe k))

mono :: MonoType (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k)

equivalent :: SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) -> Bool

(Ord m, Ord p, Ord k, Inferable (SystemFOmega m p) k, (~) * (TypingContext (SystemFOmega m p) k) (InferenceContext (SystemFOmega m p) k)) => HigherOrder (SystemFOmega m p (Maybe k))

Associated Types

type Kindsystem (SystemFOmega m p (Maybe k)) :: *

type KindContext (SystemFOmega m p (Maybe k)) :: *

type KindError (SystemFOmega m p (Maybe k)) :: *

Methods

kindcheck :: KindContext (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k) -> Either [KindError (SystemFOmega m p (Maybe k))] (KindContext (SystemFOmega m p (Maybe k)), Kindsystem (SystemFOmega m p (Maybe k)))

typeap :: SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k)

untypeap :: SystemFOmega m p (Maybe k) -> Maybe (SystemFOmega m p (Maybe k), SystemFOmega m p (Maybe k))

(Ord m, Ord p, Ord k) => Polymorphic (SystemFOmega m p (Maybe k))

Associated Types

type PolyType (SystemFOmega m p (Maybe k)) :: *

Methods

substitutions :: SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) -> Either [(SystemFOmega m p (Maybe k), SystemFOmega m p (Maybe k))] [Substitution (SystemFOmega m p (Maybe k)) (PolyType (SystemFOmega m p (Maybe k)))]

applySubstitution :: SystemFOmega m p (Maybe k) -> PolyType (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k)

quantify :: PolyType (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k)

poly :: PolyType (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k)

polytypesOf :: SystemFOmega m p (Maybe k) -> Set (SystemFOmega m p (Maybe k))

quantifiedOf :: SystemFOmega m p (Maybe k) -> Set (SystemFOmega m p (Maybe k))

type MonoType (SystemFOmega m p (Maybe k))

type MonoType (SystemFOmega m p (Maybe k)) = m

type Kindsystem (SystemFOmega m p (Maybe k))

type Kindsystem (SystemFOmega m p (Maybe k)) = k

type KindContext (SystemFOmega m p (Maybe k))

type KindContext (SystemFOmega m p (Maybe k)) = TypingContext (SystemFOmega m p) k

type KindError (SystemFOmega m p (Maybe k))

type KindError (SystemFOmega m p (Maybe k)) = Either (InferError (SystemFOmega m p) k) (TypeError (SystemFOmega m p) k)

type PolyType (SystemFOmega m p (Maybe k))

type PolyType (SystemFOmega m p (Maybe k)) = p

markAsFunctionArrow :: Eq m => m -> SystemFOmega m p k -> SystemFOmega m p k

Given a function arrow representation of type m, replace all matching mono types with the function arrow.