Copyright | Brent Yorgey |
---|---|
License | BSD-3-Clause |
Maintainer | byorgey@gmail.com |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Types for the Swarm programming language and related utilities.
Synopsis
- data BaseTy
- type Var = Text
- data TypeF t
- type Type = Fix TypeF
- tyVars :: Type -> Set Var
- pattern TyBase :: BaseTy -> Type
- pattern TyVar :: Var -> Type
- pattern TyUnit :: Type
- pattern TyInt :: Type
- pattern TyText :: Type
- pattern TyDir :: Type
- pattern TyBool :: Type
- pattern TyRobot :: Type
- pattern (:+:) :: Type -> Type -> Type
- pattern (:*:) :: Type -> Type -> Type
- pattern (:->:) :: Type -> Type -> Type
- pattern TyCmd :: Type -> Type
- pattern TyDelay :: Type -> Type
- type UType = UTerm TypeF IntVar
- pattern UTyBase :: BaseTy -> UType
- pattern UTyVar :: Var -> UType
- pattern UTyUnit :: UType
- pattern UTyInt :: UType
- pattern UTyText :: UType
- pattern UTyDir :: UType
- pattern UTyBool :: UType
- pattern UTyRobot :: UType
- pattern UTySum :: UType -> UType -> UType
- pattern UTyProd :: UType -> UType -> UType
- pattern UTyFun :: UType -> UType -> UType
- pattern UTyCmd :: UType -> UType
- pattern UTyDelay :: UType -> UType
- ucata :: Functor t => (v -> a) -> (t a -> a) -> UTerm t v -> a
- mkVarName :: Text -> IntVar -> Var
- data Poly t = Forall [Var] t
- type Polytype = Poly Type
- pattern PolyUnit :: Polytype
- type UPolytype = Poly UType
- type TCtx = Ctx Polytype
- type UCtx = Ctx UPolytype
- data Module s t = Module {}
- type TModule = Module Polytype Polytype
- type UModule = Module UType UPolytype
- trivMod :: s -> Module s t
- class WithU t where
Basic definitions
Base types.
BUnit | The unit type, with a single inhabitant. |
BInt | Signed, arbitrary-size integers. |
BText | Unicode strings. |
BDir | Directions. |
BBool | Booleans. |
BRobot | Robots. |
Instances
FromJSON BaseTy Source # | |
ToJSON BaseTy Source # | |
Defined in Swarm.Language.Types | |
Data BaseTy Source # | |
Defined in Swarm.Language.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BaseTy -> c BaseTy # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BaseTy # toConstr :: BaseTy -> Constr # dataTypeOf :: BaseTy -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BaseTy) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy) # gmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r # gmapQ :: (forall d. Data d => d -> u) -> BaseTy -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BaseTy -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy # | |
Generic BaseTy Source # | |
Show BaseTy Source # | |
Eq BaseTy Source # | |
Ord BaseTy Source # | |
PrettyPrec BaseTy Source # | |
Defined in Swarm.Language.Pretty | |
type Rep BaseTy Source # | |
Defined in Swarm.Language.Types type Rep BaseTy = D1 ('MetaData "BaseTy" "Swarm.Language.Types" "swarm-0.1.1.0-ARNQOCsge3P61nb92PmOB2" 'False) ((C1 ('MetaCons "BUnit" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BInt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BText" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BDir" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BBool" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BRobot" 'PrefixI 'False) (U1 :: Type -> Type)))) |
A "structure functor" encoding the shape of type expressions.
Actual types are then represented by taking a fixed point of this
functor. We represent types in this way, via a "two-level type",
so that we can work with the unification-fd
package (see
https://byorgey.wordpress.com/2021/09/08/implementing-hindley-milner-with-the-unification-fd-library/).
TyBaseF BaseTy | A base type. |
TyVarF Var | A type variable. |
TyCmdF t | Commands, with return type. Note that commands form a monad. |
TyDelayF t | Type of delayed computations. |
TySumF t t | Sum type. |
TyProdF t t | Product type. |
TyFunF t t | Function type. |
Instances
Type
UType
Utilities
mkVarName :: Text -> IntVar -> Var Source #
A quick-and-dirty method for turning an IntVar
(used internally
as a unification variable) into a unique variable name, by
appending a number to the given name.
Polytypes
A Poly t
is a universally quantified t
. The variables in the
list are bound inside the t
. For example, the type forall
a. a -> a
would be represented as Forall ["a"] (TyFun "a" "a")
.
Instances
Functor Poly Source # | |
PrettyPrec Polytype Source # | |
Defined in Swarm.Language.Pretty | |
PrettyPrec UPolytype Source # | |
Defined in Swarm.Language.Pretty | |
HasBindings UCtx Source # | |
Defined in Swarm.Language.Typecheck | |
HasBindings UModule Source # | |
Defined in Swarm.Language.Typecheck | |
HasBindings UPolytype Source # | |
Defined in Swarm.Language.Typecheck | |
FromJSON t => FromJSON (Poly t) Source # | |
ToJSON t => ToJSON (Poly t) Source # | |
Defined in Swarm.Language.Types | |
Data t => Data (Poly t) Source # | |
Defined in Swarm.Language.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Poly t -> c (Poly t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Poly t) # toConstr :: Poly t -> Constr # dataTypeOf :: Poly t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Poly t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Poly t)) # gmapT :: (forall b. Data b => b -> b) -> Poly t -> Poly t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Poly t -> r # gmapQ :: (forall d. Data d => d -> u) -> Poly t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Poly t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Poly t -> m (Poly t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Poly t -> m (Poly t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Poly t -> m (Poly t) # | |
Generic (Poly t) Source # | |
Show t => Show (Poly t) Source # | |
Eq t => Eq (Poly t) Source # | |
type Rep (Poly t) Source # | |
Defined in Swarm.Language.Types type Rep (Poly t) = D1 ('MetaData "Poly" "Swarm.Language.Types" "swarm-0.1.1.0-ARNQOCsge3P61nb92PmOB2" 'False) (C1 ('MetaCons "Forall" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Var]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t))) |
Contexts
type TCtx = Ctx Polytype Source #
A TCtx
is a mapping from variables to polytypes. We generally
get one of these at the end of the type inference process.
type UCtx = Ctx UPolytype Source #
A UCtx
is a mapping from variables to polytypes with
unification variables. We generally have one of these while we
are in the midst of the type inference process.
Modules
A module generally represents the result of performing type
inference on a top-level expression, which in particular can
contain definitions (TDef
). A module
contains the overall type of the expression, as well as the
context giving the types of any defined variables.
Instances
HasBindings UModule Source # | |
Defined in Swarm.Language.Typecheck | |
Functor (Module s) Source # | |
(FromJSON s, FromJSON t) => FromJSON (Module s t) Source # | |
(ToJSON t, ToJSON s) => ToJSON (Module s t) Source # | |
Defined in Swarm.Language.Types | |
(Data s, Data t) => Data (Module s t) Source # | |
Defined in Swarm.Language.Types gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Module s t -> c (Module s t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Module s t) # toConstr :: Module s t -> Constr # dataTypeOf :: Module s t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Module s t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Module s t)) # gmapT :: (forall b. Data b => b -> b) -> Module s t -> Module s t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Module s t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Module s t -> r # gmapQ :: (forall d. Data d => d -> u) -> Module s t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Module s t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Module s t -> m (Module s t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Module s t -> m (Module s t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Module s t -> m (Module s t) # | |
Generic (Module s t) Source # | |
(Show s, Show t) => Show (Module s t) Source # | |
(Eq s, Eq t) => Eq (Module s t) Source # | |
type Rep (Module s t) Source # | |
Defined in Swarm.Language.Types type Rep (Module s t) = D1 ('MetaData "Module" "Swarm.Language.Types" "swarm-0.1.1.0-ARNQOCsge3P61nb92PmOB2" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) (S1 ('MetaSel ('Just "moduleTy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 s) :*: S1 ('MetaSel ('Just "moduleCtx") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Ctx t)))) |
type TModule = Module Polytype Polytype Source #
A TModule
is the final result of the type inference process on
an expression: we get a polytype for the expression, and a
context of polytypes for the defined variables.
The WithU
class
In several cases we have two versions of something: a "normal"
version, and a U
version with unification variables in it
(e.g. Type
vs UType
, Polytype
vs UPolytype
, TCtx
vs
UCtx
). This class abstracts over the process of converting back
and forth between them.
In particular,
represents the fact that the type WithU
tt
also has a U
counterpart, with a way to convert back and forth.
Note, however, that converting back may be "unsafe" in the sense
that it requires an extra burden of proof to guarantee that it is
used only on inputs that are safe.
Convert from t
to its associated "U
-version". This
direction is always safe (we simply have no unification
variables even though the type allows it).
Convert from the associated "U
-version" back to t
.
Generally, this direction requires somehow knowing that there
are no longer any unification variables in the value being
converted.
Orphan instances
Data IntVar Source # | |
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IntVar -> c IntVar # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IntVar # toConstr :: IntVar -> Constr # dataTypeOf :: IntVar -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IntVar) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IntVar) # gmapT :: (forall b. Data b => b -> b) -> IntVar -> IntVar # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IntVar -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IntVar -> r # gmapQ :: (forall d. Data d => d -> u) -> IntVar -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IntVar -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IntVar -> m IntVar # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IntVar -> m IntVar # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IntVar -> m IntVar # |