swarm-0.2.0.0: 2D resource gathering game with programmable robots
CopyrightBrent Yorgey
LicenseBSD-3-Clause
Maintainerbyorgey@gmail.com
Safe HaskellSafe-Inferred
LanguageHaskell2010

Swarm.Language.Types

Description

Types for the Swarm programming language and related utilities.

Synopsis

Basic definitions

data BaseTy Source #

Base types.

Constructors

BVoid

The void type, with no inhabitants.

BUnit

The unit type, with a single inhabitant.

BInt

Signed, arbitrary-size integers.

BText

Unicode strings.

BDir

Directions.

BBool

Booleans.

BRobot

Robots.

Instances

Instances details
FromJSON BaseTy Source # 
Instance details

Defined in Swarm.Language.Types

ToJSON BaseTy Source # 
Instance details

Defined in Swarm.Language.Types

Data BaseTy Source # 
Instance details

Defined in Swarm.Language.Types

Methods

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 # 
Instance details

Defined in Swarm.Language.Types

Associated Types

type Rep BaseTy :: Type -> Type #

Methods

from :: BaseTy -> Rep BaseTy x #

to :: Rep BaseTy x -> BaseTy #

Show BaseTy Source # 
Instance details

Defined in Swarm.Language.Types

Eq BaseTy Source # 
Instance details

Defined in Swarm.Language.Types

Methods

(==) :: BaseTy -> BaseTy -> Bool #

(/=) :: BaseTy -> BaseTy -> Bool #

Ord BaseTy Source # 
Instance details

Defined in Swarm.Language.Types

PrettyPrec BaseTy Source # 
Instance details

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> BaseTy -> Doc ann Source #

type Rep BaseTy Source # 
Instance details

Defined in Swarm.Language.Types

type Rep BaseTy = D1 ('MetaData "BaseTy" "Swarm.Language.Types" "swarm-0.2.0.0-D1mAmWsUEjoFqpCaq9DHG0" 'False) ((C1 ('MetaCons "BVoid" 'PrefixI 'False) (U1 :: Type -> Type) :+: (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))))

type Var = Text Source #

We use Text values to represent variables.

data TypeF t Source #

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/).

Constructors

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

Instances details
FromJSON Type Source # 
Instance details

Defined in Swarm.Language.Types

ToJSON Type Source # 
Instance details

Defined in Swarm.Language.Types

Data Type Source # 
Instance details

Defined in Swarm.Language.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type #

toConstr :: Type -> Constr #

dataTypeOf :: Type -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) #

gmapT :: (forall b. Data b => b -> b) -> Type -> Type #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r #

gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type #

Data UType Source # 
Instance details

Defined in Swarm.Language.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UType -> c UType #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UType #

toConstr :: UType -> Constr #

dataTypeOf :: UType -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UType) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UType) #

gmapT :: (forall b. Data b => b -> b) -> UType -> UType #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UType -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UType -> r #

gmapQ :: (forall d. Data d => d -> u) -> UType -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UType -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UType -> m UType #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UType -> m UType #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UType -> m UType #

Foldable TypeF Source # 
Instance details

Defined in Swarm.Language.Types

Methods

fold :: Monoid m => TypeF m -> m #

foldMap :: Monoid m => (a -> m) -> TypeF a -> m #

foldMap' :: Monoid m => (a -> m) -> TypeF a -> m #

foldr :: (a -> b -> b) -> b -> TypeF a -> b #

foldr' :: (a -> b -> b) -> b -> TypeF a -> b #

foldl :: (b -> a -> b) -> b -> TypeF a -> b #

foldl' :: (b -> a -> b) -> b -> TypeF a -> b #

foldr1 :: (a -> a -> a) -> TypeF a -> a #

foldl1 :: (a -> a -> a) -> TypeF a -> a #

toList :: TypeF a -> [a] #

null :: TypeF a -> Bool #

length :: TypeF a -> Int #

elem :: Eq a => a -> TypeF a -> Bool #

maximum :: Ord a => TypeF a -> a #

minimum :: Ord a => TypeF a -> a #

sum :: Num a => TypeF a -> a #

product :: Num a => TypeF a -> a #

IsString Type Source #

For convenience, so we can write e.g. "a" instead of TyVar "a".

Instance details

Defined in Swarm.Language.Types

Methods

fromString :: String -> Type #

IsString UType Source # 
Instance details

Defined in Swarm.Language.Types

Methods

fromString :: String -> UType #

Traversable TypeF Source # 
Instance details

Defined in Swarm.Language.Types

Methods

traverse :: Applicative f => (a -> f b) -> TypeF a -> f (TypeF b) #

sequenceA :: Applicative f => TypeF (f a) -> f (TypeF a) #

mapM :: Monad m => (a -> m b) -> TypeF a -> m (TypeF b) #

sequence :: Monad m => TypeF (m a) -> m (TypeF a) #

Functor TypeF Source # 
Instance details

Defined in Swarm.Language.Types

Methods

fmap :: (a -> b) -> TypeF a -> TypeF b #

(<$) :: a -> TypeF b -> TypeF a #

Generic Type Source # 
Instance details

Defined in Swarm.Language.Types

Associated Types

type Rep Type :: Type -> Type #

Methods

from :: Type -> Rep Type x #

to :: Rep Type x -> Type #

PrettyPrec Polytype Source # 
Instance details

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> Polytype -> Doc ann Source #

PrettyPrec UPolytype Source # 
Instance details

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> UPolytype -> Doc ann Source #

HasBindings UCtx Source # 
Instance details

Defined in Swarm.Language.Typecheck

HasBindings UModule Source # 
Instance details

Defined in Swarm.Language.Typecheck

HasBindings UPolytype Source # 
Instance details

Defined in Swarm.Language.Typecheck

HasBindings UType Source # 
Instance details

Defined in Swarm.Language.Typecheck

WithU Type Source #

Type is an instance of WithU, with associated type UType.

Instance details

Defined in Swarm.Language.Types

Associated Types

type U Type Source #

Methods

toU :: Type -> U Type Source #

fromU :: U Type -> Type Source #

Unifiable TypeF Source # 
Instance details

Defined in Swarm.Language.Types

Methods

zipMatch :: TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a))) #

Generic1 TypeF Source # 
Instance details

Defined in Swarm.Language.Types

Associated Types

type Rep1 TypeF :: k -> Type #

Methods

from1 :: forall (a :: k). TypeF a -> Rep1 TypeF a #

to1 :: forall (a :: k). Rep1 TypeF a -> TypeF a #

Fallible TypeF IntVar TypeErr Source # 
Instance details

Defined in Swarm.Language.Typecheck

FromJSON t => FromJSON (TypeF t) Source # 
Instance details

Defined in Swarm.Language.Types

ToJSON t => ToJSON (TypeF t) Source # 
Instance details

Defined in Swarm.Language.Types

Data t => Data (TypeF t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeF t -> c (TypeF t) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypeF t) #

toConstr :: TypeF t -> Constr #

dataTypeOf :: TypeF t -> DataType #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (TypeF t)) #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (TypeF t)) #

gmapT :: (forall b. Data b => b -> b) -> TypeF t -> TypeF t #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeF t -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeF t -> r #

gmapQ :: (forall d. Data d => d -> u) -> TypeF t -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeF t -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeF t -> m (TypeF t) #

Generic (TypeF t) Source # 
Instance details

Defined in Swarm.Language.Types

Associated Types

type Rep (TypeF t) :: Type -> Type #

Methods

from :: TypeF t -> Rep (TypeF t) x #

to :: Rep (TypeF t) x -> TypeF t #

Show t => Show (TypeF t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> TypeF t -> ShowS #

show :: TypeF t -> String #

showList :: [TypeF t] -> ShowS #

Eq t => Eq (TypeF t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

(==) :: TypeF t -> TypeF t -> Bool #

(/=) :: TypeF t -> TypeF t -> Bool #

PrettyPrec t => PrettyPrec (TypeF t) Source # 
Instance details

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> TypeF t -> Doc ann Source #

type Rep Type Source # 
Instance details

Defined in Swarm.Language.Types

type Rep Type = D1 ('MetaData "Fix" "Data.Functor.Fixedpoint" "unification-fd-0.11.2-10nGBFM9NSRCQtHAyha5T3" 'True) (C1 ('MetaCons "Fix" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TypeF (Fix TypeF)))))
type U Type Source # 
Instance details

Defined in Swarm.Language.Types

type U Type = UType
type Rep1 TypeF Source # 
Instance details

Defined in Swarm.Language.Types

type Rep (TypeF t) Source # 
Instance details

Defined in Swarm.Language.Types

type Rep (TypeF t) = D1 ('MetaData "TypeF" "Swarm.Language.Types" "swarm-0.2.0.0-D1mAmWsUEjoFqpCaq9DHG0" 'False) ((C1 ('MetaCons "TyBaseF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 BaseTy)) :+: (C1 ('MetaCons "TyVarF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Var)) :+: C1 ('MetaCons "TyCmdF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t)))) :+: ((C1 ('MetaCons "TyDelayF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t)) :+: C1 ('MetaCons "TySumF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t))) :+: (C1 ('MetaCons "TyProdF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t)) :+: C1 ('MetaCons "TyFunF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t)))))

Type

type Type = Fix TypeF Source #

Type is now defined as the fixed point of TypeF. It would be annoying to manually apply and match against Fix constructors everywhere, so we provide pattern synonyms that allow us to work with Type as if it were defined in a directly recursive way.

tyVars :: Type -> Set Var Source #

Get all the type variables contained in a Type.

pattern TyBase :: BaseTy -> Type Source #

pattern TyVar :: Var -> Type Source #

pattern TyVoid :: Type Source #

pattern TyUnit :: Type Source #

pattern TyInt :: Type Source #

pattern TyText :: Type Source #

pattern TyDir :: Type Source #

pattern TyBool :: Type Source #

pattern TyRobot :: Type Source #

pattern (:+:) :: Type -> Type -> Type infixr 5 Source #

pattern (:*:) :: Type -> Type -> Type infixr 6 Source #

pattern (:->:) :: Type -> Type -> Type infixr 1 Source #

pattern TyCmd :: Type -> Type Source #

pattern TyDelay :: Type -> Type Source #

UType

type UType = UTerm TypeF IntVar Source #

UTypes are like Types, but also contain unification variables. UType is defined via UTerm, which is also a kind of fixed point (in fact, UType is the free monad over TypeF).

Just as with Type, we provide a bunch of pattern synonyms for working with UType as if it were defined directly.

pattern UTyBase :: BaseTy -> UType Source #

pattern UTyVar :: Var -> UType Source #

pattern UTyVoid :: UType Source #

pattern UTyUnit :: UType Source #

pattern UTyInt :: UType Source #

pattern UTyText :: UType Source #

pattern UTyDir :: UType Source #

pattern UTyBool :: UType Source #

pattern UTyRobot :: UType Source #

pattern UTySum :: UType -> UType -> UType Source #

pattern UTyProd :: UType -> UType -> UType Source #

pattern UTyFun :: UType -> UType -> UType Source #

pattern UTyCmd :: UType -> UType Source #

pattern UTyDelay :: UType -> UType Source #

Utilities

ucata :: Functor t => (v -> a) -> (t a -> a) -> UTerm t v -> a Source #

A generic fold for things defined via UTerm (including, in particular, UType). This probably belongs in the unification-fd package, but since it doesn't provide one, we define it here.

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

data Poly t Source #

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").

Constructors

Forall [Var] t 

Instances

Instances details
Functor Poly Source # 
Instance details

Defined in Swarm.Language.Types

Methods

fmap :: (a -> b) -> Poly a -> Poly b #

(<$) :: a -> Poly b -> Poly a #

PrettyPrec Polytype Source # 
Instance details

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> Polytype -> Doc ann Source #

PrettyPrec UPolytype Source # 
Instance details

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> UPolytype -> Doc ann Source #

HasBindings UCtx Source # 
Instance details

Defined in Swarm.Language.Typecheck

HasBindings UModule Source # 
Instance details

Defined in Swarm.Language.Typecheck

HasBindings UPolytype Source # 
Instance details

Defined in Swarm.Language.Typecheck

FromJSON t => FromJSON (Poly t) Source # 
Instance details

Defined in Swarm.Language.Types

ToJSON t => ToJSON (Poly t) Source # 
Instance details

Defined in Swarm.Language.Types

Data t => Data (Poly t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

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 # 
Instance details

Defined in Swarm.Language.Types

Associated Types

type Rep (Poly t) :: Type -> Type #

Methods

from :: Poly t -> Rep (Poly t) x #

to :: Rep (Poly t) x -> Poly t #

Show t => Show (Poly t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> Poly t -> ShowS #

show :: Poly t -> String #

showList :: [Poly t] -> ShowS #

Eq t => Eq (Poly t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

(==) :: Poly t -> Poly t -> Bool #

(/=) :: Poly t -> Poly t -> Bool #

type Rep (Poly t) Source # 
Instance details

Defined in Swarm.Language.Types

type Rep (Poly t) = D1 ('MetaData "Poly" "Swarm.Language.Types" "swarm-0.2.0.0-D1mAmWsUEjoFqpCaq9DHG0" '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)))

type Polytype = Poly Type Source #

A polytype without unification variables.

type UPolytype = Poly UType Source #

A polytype with unification variables.

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

data Module s t Source #

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.

Constructors

Module 

Fields

Instances

Instances details
HasBindings UModule Source # 
Instance details

Defined in Swarm.Language.Typecheck

Functor (Module s) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

fmap :: (a -> b) -> Module s a -> Module s b #

(<$) :: a -> Module s b -> Module s a #

(FromJSON s, FromJSON t) => FromJSON (Module s t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

parseJSON :: Value -> Parser (Module s t) #

parseJSONList :: Value -> Parser [Module s t] #

(ToJSON t, ToJSON s) => ToJSON (Module s t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

toJSON :: Module s t -> Value #

toEncoding :: Module s t -> Encoding #

toJSONList :: [Module s t] -> Value #

toEncodingList :: [Module s t] -> Encoding #

(Data s, Data t) => Data (Module s t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

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 # 
Instance details

Defined in Swarm.Language.Types

Associated Types

type Rep (Module s t) :: Type -> Type #

Methods

from :: Module s t -> Rep (Module s t) x #

to :: Rep (Module s t) x -> Module s t #

(Show s, Show t) => Show (Module s t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> Module s t -> ShowS #

show :: Module s t -> String #

showList :: [Module s t] -> ShowS #

(Eq s, Eq t) => Eq (Module s t) Source # 
Instance details

Defined in Swarm.Language.Types

Methods

(==) :: Module s t -> Module s t -> Bool #

(/=) :: Module s t -> Module s t -> Bool #

type Rep (Module s t) Source # 
Instance details

Defined in Swarm.Language.Types

type Rep (Module s t) = D1 ('MetaData "Module" "Swarm.Language.Types" "swarm-0.2.0.0-D1mAmWsUEjoFqpCaq9DHG0" '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.

type UModule = Module UType UPolytype Source #

A UModule represents the type of an expression at some intermediate stage during the type inference process. We get a UType (not a UPolytype) for the expression, which may contain some free unification or type variables, as well as a context of UPolytypes for any defined variables.

trivMod :: s -> Module s t Source #

The trivial module for a given s, with the empty context.

The WithU class

class WithU t where Source #

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, WithU t represents the fact that the type t 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.

Associated Types

type U t :: * Source #

The associated "U-version" of the type t.

Methods

toU :: t -> U t Source #

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).

fromU :: U t -> t Source #

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.

Instances

Instances details
WithU Type Source #

Type is an instance of WithU, with associated type UType.

Instance details

Defined in Swarm.Language.Types

Associated Types

type U Type Source #

Methods

toU :: Type -> U Type Source #

fromU :: U Type -> Type Source #

(WithU t, Functor f) => WithU (f t) Source #

A WithU instance can be lifted through any functor (including, in particular, Ctx and Poly).

Instance details

Defined in Swarm.Language.Types

Associated Types

type U (f t) Source #

Methods

toU :: f t -> U (f t) Source #

fromU :: U (f t) -> f t Source #

Orphan instances

Data IntVar Source # 
Instance details

Methods

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 #