Swarm.Language.Types

Types for the Swarm programming language and related utilities.

Basic definitions

Base types and type constructors

data BaseTy

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.

BActor

Actors, i.e. anything that can do stuff. Internally, these are all just "robots", but we give them a more generic in-game name because they could represent other things like aliens, animals, seeds, ...

BKey

Keys, i.e. things that can be pressed on the keyboard

Instances

FromJSON BaseTy

Defined in Swarm.Language.Types

Methods

parseJSON :: Value -> Parser BaseTy

parseJSONList :: Value -> Parser [BaseTy]

omittedField :: Maybe BaseTy

ToJSON BaseTy

Defined in Swarm.Language.Types

Methods

toJSON :: BaseTy -> Value

toEncoding :: BaseTy -> Encoding

toJSONList :: [BaseTy] -> Value

toEncodingList :: [BaseTy] -> Encoding

omitField :: BaseTy -> Bool

Data BaseTy

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

Bounded BaseTy

Defined in Swarm.Language.Types

Methods

minBound :: BaseTy

maxBound :: BaseTy

Enum BaseTy

Defined in Swarm.Language.Types

Methods

succ :: BaseTy -> BaseTy

pred :: BaseTy -> BaseTy

toEnum :: Int -> BaseTy

fromEnum :: BaseTy -> Int

enumFrom :: BaseTy -> [BaseTy]

enumFromThen :: BaseTy -> BaseTy -> [BaseTy]

enumFromTo :: BaseTy -> BaseTy -> [BaseTy]

enumFromThenTo :: BaseTy -> BaseTy -> BaseTy -> [BaseTy]

Generic BaseTy

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

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> BaseTy -> ShowS

show :: BaseTy -> String

showList :: [BaseTy] -> ShowS

Eq BaseTy

Defined in Swarm.Language.Types

Methods

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

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

Ord BaseTy

Defined in Swarm.Language.Types

Methods

compare :: BaseTy -> BaseTy -> Ordering

(<) :: BaseTy -> BaseTy -> Bool

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

(>) :: BaseTy -> BaseTy -> Bool

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

max :: BaseTy -> BaseTy -> BaseTy

min :: BaseTy -> BaseTy -> BaseTy

PrettyPrec BaseTy

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> BaseTy -> Doc ann

type Rep BaseTy

Defined in Swarm.Language.Types

type Rep BaseTy = D1 ('MetaData "BaseTy" "Swarm.Language.Types" "swarm-0.6.0.0-ERx1HMcRMba59aI2b6aNrS-swarm-lang" '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 "BActor" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BKey" 'PrefixI 'False) (U1 :: Type -> Type))))

baseTyName :: BaseTy -> Text

data TyCon

Type constructors.

Constructors

TCBase BaseTy

Base types are (nullary) type constructors.

TCCmd

Command types.

TCDelay

Delayed computations.

TCSum

Sum types.

TCProd

Product types.

TCFun

Function types.

TCUser Var

User-defined type constructor.

Instances

FromJSON TyCon

Defined in Swarm.Language.Types

Methods

parseJSON :: Value -> Parser TyCon

parseJSONList :: Value -> Parser [TyCon]

omittedField :: Maybe TyCon

ToJSON TyCon

Defined in Swarm.Language.Types

Methods

toJSON :: TyCon -> Value

toEncoding :: TyCon -> Encoding

toJSONList :: [TyCon] -> Value

toEncodingList :: [TyCon] -> Encoding

omitField :: TyCon -> Bool

Data TyCon

Defined in Swarm.Language.Types

Methods

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

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

toConstr :: TyCon -> Constr

dataTypeOf :: TyCon -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TyCon -> TyCon

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

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

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

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

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

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

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

Generic TyCon

Defined in Swarm.Language.Types

Associated Types

type Rep TyCon :: Type -> Type

Methods

from :: TyCon -> Rep TyCon x

to :: Rep TyCon x -> TyCon

Show TyCon

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> TyCon -> ShowS

show :: TyCon -> String

showList :: [TyCon] -> ShowS

Eq TyCon

Defined in Swarm.Language.Types

Methods

(==) :: TyCon -> TyCon -> Bool

(/=) :: TyCon -> TyCon -> Bool

Ord TyCon

Defined in Swarm.Language.Types

Methods

compare :: TyCon -> TyCon -> Ordering

(<) :: TyCon -> TyCon -> Bool

(<=) :: TyCon -> TyCon -> Bool

(>) :: TyCon -> TyCon -> Bool

(>=) :: TyCon -> TyCon -> Bool

max :: TyCon -> TyCon -> TyCon

min :: TyCon -> TyCon -> TyCon

PrettyPrec TyCon

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> TyCon -> Doc ann

type Rep TyCon

Defined in Swarm.Language.Types

type Rep TyCon = D1 ('MetaData "TyCon" "Swarm.Language.Types" "swarm-0.6.0.0-ERx1HMcRMba59aI2b6aNrS-swarm-lang" 'False) ((C1 ('MetaCons "TCBase" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 BaseTy)) :+: (C1 ('MetaCons "TCCmd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCDelay" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TCSum" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCProd" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TCFun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCUser" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Var)))))

newtype Arity

The arity of a type, i.e. the number of type parameters it expects.

Constructors

Arity

Fields

• getArity :: Int

Instances

FromJSON Arity

Defined in Swarm.Language.Types

Methods

parseJSON :: Value -> Parser Arity

parseJSONList :: Value -> Parser [Arity]

omittedField :: Maybe Arity

ToJSON Arity

Defined in Swarm.Language.Types

Methods

toJSON :: Arity -> Value

toEncoding :: Arity -> Encoding

toJSONList :: [Arity] -> Value

toEncodingList :: [Arity] -> Encoding

omitField :: Arity -> Bool

Data Arity

Defined in Swarm.Language.Types

Methods

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

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

toConstr :: Arity -> Constr

dataTypeOf :: Arity -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Arity -> Arity

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

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

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

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

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

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

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

Generic Arity

Defined in Swarm.Language.Types

Associated Types

type Rep Arity :: Type -> Type

Methods

from :: Arity -> Rep Arity x

to :: Rep Arity x -> Arity

Show Arity

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> Arity -> ShowS

show :: Arity -> String

showList :: [Arity] -> ShowS

Eq Arity

Defined in Swarm.Language.Types

Methods

(==) :: Arity -> Arity -> Bool

(/=) :: Arity -> Arity -> Bool

Ord Arity

Defined in Swarm.Language.Types

Methods

compare :: Arity -> Arity -> Ordering

(<) :: Arity -> Arity -> Bool

(<=) :: Arity -> Arity -> Bool

(>) :: Arity -> Arity -> Bool

(>=) :: Arity -> Arity -> Bool

max :: Arity -> Arity -> Arity

min :: Arity -> Arity -> Arity

PrettyPrec Arity

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> Arity -> Doc ann

type Rep Arity

Defined in Swarm.Language.Types

type Rep Arity = D1 ('MetaData "Arity" "Swarm.Language.Types" "swarm-0.6.0.0-ERx1HMcRMba59aI2b6aNrS-swarm-lang" 'True) (C1 ('MetaCons "Arity" 'PrefixI 'True) (S1 ('MetaSel ('Just "getArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

tcArity :: TDCtx -> TyCon -> Maybe Arity

The arity, i.e. number of type arguments, of each type constructor. Eventually, if we generalize to higher-kinded types, we'll need to upgrade this to return a full-fledged kind instead of just an arity.

type Var = Text

We use Text values to represent variables.

Type structure functor

data TypeF t

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 easily use generic recursion schemes to implement things like substitution.

Constructors

TyConF TyCon [t]

A type constructor applied to some type arguments. For now, all type constructor applications are required to be fully saturated (higher kinds are not supported), so we just directly store a list of all arguments (as opposed to iterating binary application).

TyVarF Var

A type variable.

TyRcdF (Map Var t)

Record type.

TyRecVarF Nat

A recursive type variable bound by an enclosing Rec, represented by a de Bruijn index.

TyRecF Var t

Recursive type. The variable is just a suggestion for a name to use when pretty-printing; the actual bound variables are represented via de Bruijn indices.

Instances

FromJSON TSyntax

Defined in Swarm.Language.JSON

Methods

parseJSON :: Value -> Parser TSyntax

parseJSONList :: Value -> Parser [TSyntax]

omittedField :: Maybe TSyntax

FromJSON1 TypeF

Defined in Swarm.Language.Types

Methods

liftParseJSON :: Maybe a -> (Value -> Parser a) -> (Value -> Parser [a]) -> Value -> Parser (TypeF a)

liftParseJSONList :: Maybe a -> (Value -> Parser a) -> (Value -> Parser [a]) -> Value -> Parser [TypeF a]

liftOmittedField :: Maybe a -> Maybe (TypeF a)

ToJSON TSyntax

Defined in Swarm.Language.JSON

Methods

toJSON :: TSyntax -> Value

toEncoding :: TSyntax -> Encoding

toJSONList :: [TSyntax] -> Value

toEncodingList :: [TSyntax] -> Encoding

omitField :: TSyntax -> Bool

ToJSON1 TypeF

Defined in Swarm.Language.Types

Methods

liftToJSON :: (a -> Bool) -> (a -> Value) -> ([a] -> Value) -> TypeF a -> Value

liftToJSONList :: (a -> Bool) -> (a -> Value) -> ([a] -> Value) -> [TypeF a] -> Value

liftToEncoding :: (a -> Bool) -> (a -> Encoding) -> ([a] -> Encoding) -> TypeF a -> Encoding

liftToEncodingList :: (a -> Bool) -> (a -> Encoding) -> ([a] -> Encoding) -> [TypeF a] -> Encoding

liftOmitField :: (a -> Bool) -> TypeF a -> Bool

Foldable TypeF

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

Eq1 TypeF

Defined in Swarm.Language.Types

Methods

liftEq :: (a -> b -> Bool) -> TypeF a -> TypeF b -> Bool

Ord1 TypeF

Defined in Swarm.Language.Types

Methods

liftCompare :: (a -> b -> Ordering) -> TypeF a -> TypeF b -> Ordering

Show1 TypeF

Defined in Swarm.Language.Types

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> TypeF a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [TypeF a] -> ShowS

IsString Type

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

Defined in Swarm.Language.Types

Methods

fromString :: String -> Type

IsString UType

Defined in Swarm.Language.Types

Methods

fromString :: String -> UType

Traversable TypeF

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

Defined in Swarm.Language.Types

Methods

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

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

PrettyPrec Polytype

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> Polytype -> Doc ann

PrettyPrec UPolytype

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> UPolytype -> Doc ann

UnchainableFun Type

Defined in Swarm.Language.Pretty

Methods

unchainFun :: Type -> NonEmpty Type

SubstRec Type

Defined in Swarm.Language.Types

Methods

substRec :: TypeF Type -> Type -> Nat -> Type

WithU Type

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

Defined in Swarm.Language.Types

Associated Types

type U Type

Methods

toU :: Type -> U Type

fromU :: U Type -> Maybe Type

Generic1 TypeF

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

Substitutes IntVar UType UType

We can perform substitution on terms built up as the free monad over a structure functor f.

Defined in Swarm.Effect.Unify.Fast

Methods

subst :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has (Throw UnificationError) sig m => Subst IntVar UType -> UType -> m UType

Data t => Data (TypeF t)

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)

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)

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> TypeF t -> ShowS

show :: TypeF t -> String

showList :: [TypeF t] -> ShowS

Eq t => Eq (TypeF t)

Defined in Swarm.Language.Types

Methods

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

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

Ord t => Ord (TypeF t)

Defined in Swarm.Language.Types

Methods

compare :: TypeF t -> TypeF t -> Ordering

(<) :: TypeF t -> TypeF t -> Bool

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

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

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

max :: TypeF t -> TypeF t -> TypeF t

min :: TypeF t -> TypeF t -> TypeF t

(UnchainableFun t, PrettyPrec t, SubstRec t) => PrettyPrec (TypeF t)

Defined in Swarm.Language.Pretty

Methods

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

UnchainableFun (Free TypeF ty)

Defined in Swarm.Language.Pretty

Methods

unchainFun :: Free TypeF ty -> NonEmpty (Free TypeF ty)

SubstRec (Free TypeF v)

Defined in Swarm.Language.Types

Methods

substRec :: TypeF (Free TypeF v) -> Free TypeF v -> Nat -> Free TypeF v

type U Type

Defined in Swarm.Language.Types

type U Type = UType

type Rep1 TypeF

Defined in Swarm.Language.Types

type Rep1 TypeF = D1 ('MetaData "TypeF" "Swarm.Language.Types" "swarm-0.6.0.0-ERx1HMcRMba59aI2b6aNrS-swarm-lang" 'False) ((C1 ('MetaCons "TyConF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 TyCon) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec1 List)) :+: C1 ('MetaCons "TyVarF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Var))) :+: (C1 ('MetaCons "TyRcdF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec1 (Map Var))) :+: (C1 ('MetaCons "TyRecVarF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Nat)) :+: C1 ('MetaCons "TyRecF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Var) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) Par1))))

type Rep (TypeF t)

Defined in Swarm.Language.Types

type Rep (TypeF t) = D1 ('MetaData "TypeF" "Swarm.Language.Types" "swarm-0.6.0.0-ERx1HMcRMba59aI2b6aNrS-swarm-lang" 'False) ((C1 ('MetaCons "TyConF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 TyCon) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [t])) :+: C1 ('MetaCons "TyVarF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Var))) :+: (C1 ('MetaCons "TyRcdF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Map Var t))) :+: (C1 ('MetaCons "TyRecVarF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Nat)) :+: C1 ('MetaCons "TyRecF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Var) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t)))))

Recursive types

data Nat where

Peano naturals, for use as de Bruijn indices in recursive types.

Constructors

NZ :: Nat

NS :: Nat -> Nat

Instances

FromJSON Nat

Defined in Swarm.Language.Types

Methods

parseJSON :: Value -> Parser Nat

parseJSONList :: Value -> Parser [Nat]

omittedField :: Maybe Nat

ToJSON Nat

Defined in Swarm.Language.Types

Methods

toJSON :: Nat -> Value

toEncoding :: Nat -> Encoding

toJSONList :: [Nat] -> Value

toEncodingList :: [Nat] -> Encoding

omitField :: Nat -> Bool

Data Nat

Defined in Swarm.Language.Types

Methods

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

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

toConstr :: Nat -> Constr

dataTypeOf :: Nat -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat

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

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

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

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

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

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

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

Generic Nat

Defined in Swarm.Language.Types

Associated Types

type Rep Nat :: Type -> Type

Methods

from :: Nat -> Rep Nat x

to :: Rep Nat x -> Nat

Show Nat

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

Eq Nat

Defined in Swarm.Language.Types

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Ord Nat

Defined in Swarm.Language.Types

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

type Rep Nat

Defined in Swarm.Language.Types

type Rep Nat = D1 ('MetaData "Nat" "Swarm.Language.Types" "swarm-0.6.0.0-ERx1HMcRMba59aI2b6aNrS-swarm-lang" 'False) (C1 ('MetaCons "NZ" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Nat)))

natToInt :: Nat -> Int

unfoldRec :: SubstRec t => Var -> t -> t

unfoldRec x t unfolds the recursive type rec x. t one step, to t [(rec x. t) / x].

class SubstRec t where

Class of type-like things where we can substitute for a bound de Bruijn variable.

Methods

substRec :: TypeF t -> t -> Nat -> t

substRec s t n substitutes s for the bound de Bruijn variable n everywhere in t.

Instances

SubstRec Type

Defined in Swarm.Language.Types

Methods

substRec :: TypeF Type -> Type -> Nat -> Type

SubstRec (Free TypeF v)

Defined in Swarm.Language.Types

Methods

substRec :: TypeF (Free TypeF v) -> Free TypeF v -> Nat -> Free TypeF v

Type

type Type = Fix TypeF

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

Get all the type variables contained in a Type.

pattern TyConApp :: TyCon -> [Type] -> Type

pattern TyBase :: BaseTy -> Type

pattern TyVar :: Var -> Type

pattern TyVoid :: Type

pattern TyUnit :: Type

pattern TyInt :: Type

pattern TyText :: Type

pattern TyDir :: Type

pattern TyBool :: Type

pattern TyActor :: Type

pattern TyKey :: Type

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

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

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

pattern TyRcd :: Map Var Type -> Type

pattern TyCmd :: Type -> Type

pattern TyDelay :: Type -> Type

pattern TyUser :: Var -> [Type] -> Type

pattern TyRec :: Var -> Type -> Type

UType

newtype IntVar

Constructors

IntVar Int

Instances

Data IntVar

Defined in Swarm.Language.Types

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

IsString UType

Defined in Swarm.Language.Types

Methods

fromString :: String -> UType

Show IntVar

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> IntVar -> ShowS

show :: IntVar -> String

showList :: [IntVar] -> ShowS

Eq IntVar

Defined in Swarm.Language.Types

Methods

(==) :: IntVar -> IntVar -> Bool

(/=) :: IntVar -> IntVar -> Bool

Ord IntVar

Defined in Swarm.Language.Types

Methods

compare :: IntVar -> IntVar -> Ordering

(<) :: IntVar -> IntVar -> Bool

(<=) :: IntVar -> IntVar -> Bool

(>) :: IntVar -> IntVar -> Bool

(>=) :: IntVar -> IntVar -> Bool

max :: IntVar -> IntVar -> IntVar

min :: IntVar -> IntVar -> IntVar

PrettyPrec IntVar

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> IntVar -> Doc ann

PrettyPrec UPolytype

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> UPolytype -> Doc ann

Substitutes IntVar UType UType

We can perform substitution on terms built up as the free monad over a structure functor f.

Defined in Swarm.Effect.Unify.Fast

Methods

subst :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has (Throw UnificationError) sig m => Subst IntVar UType -> UType -> m UType

type UType = Free TypeF IntVar

UTypes are like Types, but also contain unification variables. UType is defined via Free, which is also a kind of fixed point (in fact, Free TypeF 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 UTyConApp :: TyCon -> [UType] -> UType

pattern UTyBase :: BaseTy -> UType

pattern UTyVar :: Var -> UType

pattern UTyVoid :: UType

pattern UTyUnit :: UType

pattern UTyInt :: UType

pattern UTyText :: UType

pattern UTyDir :: UType

pattern UTyBool :: UType

pattern UTyActor :: UType

pattern UTyKey :: UType

pattern UTySum :: UType -> UType -> UType

pattern UTyProd :: UType -> UType -> UType

pattern UTyFun :: UType -> UType -> UType

pattern UTyRcd :: Map Var UType -> UType

pattern UTyCmd :: UType -> UType

pattern UTyDelay :: UType -> UType

pattern UTyUser :: Var -> [UType] -> UType

pattern UTyRec :: Var -> UType -> UType

Utilities

ucata :: Functor t => (v -> a) -> (t a -> a) -> Free t v -> a

A generic fold for things defined via Free (including, in particular, UType).

mkVarName :: Text -> IntVar -> Var

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.

fuvs :: UType -> Set IntVar

Get all the free unification variables in a UType.

Polytypes

data Poly t

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

Fields

• ptVars :: [Var]
• ptBody :: t

Instances

FromJSON TSyntax

Defined in Swarm.Language.JSON

Methods

parseJSON :: Value -> Parser TSyntax

parseJSONList :: Value -> Parser [TSyntax]

omittedField :: Maybe TSyntax

ToJSON TSyntax

Defined in Swarm.Language.JSON

Methods

toJSON :: TSyntax -> Value

toEncoding :: TSyntax -> Encoding

toJSONList :: [TSyntax] -> Value

toEncodingList :: [TSyntax] -> Encoding

omitField :: TSyntax -> Bool

Foldable Poly

Defined in Swarm.Language.Types

Methods

fold :: Monoid m => Poly m -> m

foldMap :: Monoid m => (a -> m) -> Poly a -> m

foldMap' :: Monoid m => (a -> m) -> Poly a -> m

foldr :: (a -> b -> b) -> b -> Poly a -> b

foldr' :: (a -> b -> b) -> b -> Poly a -> b

foldl :: (b -> a -> b) -> b -> Poly a -> b

foldl' :: (b -> a -> b) -> b -> Poly a -> b

foldr1 :: (a -> a -> a) -> Poly a -> a

foldl1 :: (a -> a -> a) -> Poly a -> a

toList :: Poly a -> [a]

null :: Poly a -> Bool

length :: Poly a -> Int

elem :: Eq a => a -> Poly a -> Bool

maximum :: Ord a => Poly a -> a

minimum :: Ord a => Poly a -> a

sum :: Num a => Poly a -> a

product :: Num a => Poly a -> a

Traversable Poly

Defined in Swarm.Language.Types

Methods

traverse :: Applicative f => (a -> f b) -> Poly a -> f (Poly b)

sequenceA :: Applicative f => Poly (f a) -> f (Poly a)

mapM :: Monad m => (a -> m b) -> Poly a -> m (Poly b)

sequence :: Monad m => Poly (m a) -> m (Poly a)

Functor Poly

Defined in Swarm.Language.Types

Methods

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

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

PrettyPrec Polytype

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> Polytype -> Doc ann

PrettyPrec UPolytype

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> UPolytype -> Doc ann

FromJSON t => FromJSON (Poly t)

Defined in Swarm.Language.Types

Methods

parseJSON :: Value -> Parser (Poly t)

parseJSONList :: Value -> Parser [Poly t]

omittedField :: Maybe (Poly t)

ToJSON t => ToJSON (Poly t)

Defined in Swarm.Language.Types

Methods

toJSON :: Poly t -> Value

toEncoding :: Poly t -> Encoding

toJSONList :: [Poly t] -> Value

toEncodingList :: [Poly t] -> Encoding

omitField :: Poly t -> Bool

Data t => Data (Poly t)

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)

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)

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> Poly t -> ShowS

show :: Poly t -> String

showList :: [Poly t] -> ShowS

Eq t => Eq (Poly t)

Defined in Swarm.Language.Types

Methods

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

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

type Rep (Poly t)

Defined in Swarm.Language.Types

type Rep (Poly t) = D1 ('MetaData "Poly" "Swarm.Language.Types" "swarm-0.6.0.0-ERx1HMcRMba59aI2b6aNrS-swarm-lang" 'False) (C1 ('MetaCons "Forall" 'PrefixI 'True) (S1 ('MetaSel ('Just "ptVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 [Var]) :*: S1 ('MetaSel ('Just "ptBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 t)))

type Polytype = Poly Type

A polytype without unification variables.

pattern PolyUnit :: Polytype

type UPolytype = Poly UType

A polytype with unification variables.

Contexts

type TCtx = Ctx Polytype

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

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.

User type definitions

data TydefInfo

Constructors

TydefInfo

Fields

• _tydefType :: Polytype
• _tydefArity :: Arity

Instances

FromJSON TydefInfo

Defined in Swarm.Language.Types

Methods

parseJSON :: Value -> Parser TydefInfo

parseJSONList :: Value -> Parser [TydefInfo]

omittedField :: Maybe TydefInfo

ToJSON TydefInfo

Defined in Swarm.Language.Types

Methods

toJSON :: TydefInfo -> Value

toEncoding :: TydefInfo -> Encoding

toJSONList :: [TydefInfo] -> Value

toEncodingList :: [TydefInfo] -> Encoding

omitField :: TydefInfo -> Bool

Data TydefInfo

Defined in Swarm.Language.Types

Methods

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

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

toConstr :: TydefInfo -> Constr

dataTypeOf :: TydefInfo -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TydefInfo -> TydefInfo

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

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

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

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

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

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

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

Generic TydefInfo

Defined in Swarm.Language.Types

Associated Types

type Rep TydefInfo :: Type -> Type

Methods

from :: TydefInfo -> Rep TydefInfo x

to :: Rep TydefInfo x -> TydefInfo

Show TydefInfo

Defined in Swarm.Language.Types

Methods

showsPrec :: Int -> TydefInfo -> ShowS

show :: TydefInfo -> String

showList :: [TydefInfo] -> ShowS

Eq TydefInfo

Defined in Swarm.Language.Types

Methods

(==) :: TydefInfo -> TydefInfo -> Bool

(/=) :: TydefInfo -> TydefInfo -> Bool

type Rep TydefInfo

Defined in Swarm.Language.Types

type Rep TydefInfo = D1 ('MetaData "TydefInfo" "Swarm.Language.Types" "swarm-0.6.0.0-ERx1HMcRMba59aI2b6aNrS-swarm-lang" 'False) (C1 ('MetaCons "TydefInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "_tydefType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Polytype) :*: S1 ('MetaSel ('Just "_tydefArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Arity)))

tydefType :: Lens' TydefInfo Polytype

tydefArity :: Lens' TydefInfo Arity

substTydef :: forall t. Typical t => TydefInfo -> [t] -> t

Given the definition of a type alias, substitute the given arguments into its body and return the resulting type.

expandTydef :: (Has (Reader TDCtx) sig m, Typical t) => Var -> [t] -> m t

Expand an application "T ty1 ty2 ... tyn" by looking up the definition of T and substituting ty1 .. tyn for its arguments.

Note that this has already been kind-checked so we know the number of arguments must match up; we don't worry about what happens if the lists have different lengths since in theory that can never happen.

elimTydef :: forall t. Typical t => Var -> TydefInfo -> t -> t

Replace a type alias with its definition everywhere it occurs inside a type. Typically this is done when reporting the type of a term containing a local tydef: since the tydef is local we can't use it in the reported type.

type TDCtx = Ctx TydefInfo

A TDCtx is a mapping from user-defined type constructor names to their definitions and arities/kinds.

WHNF

whnfType :: TDCtx -> Type -> Type

Reduce a type to weak head normal form, i.e. keep unfold type aliases and recursive types just until the top-level constructor of the type is neither rec nor an application of a type alias.

The WithU class

class WithU t where

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 :: Type

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

Methods

toU :: t -> U t

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 -> Maybe t

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

WithU Type

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

Defined in Swarm.Language.Types

Associated Types

type U Type

Methods

toU :: Type -> U Type

fromU :: U Type -> Maybe Type

(WithU t, Traversable f) => WithU (f t)

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

Defined in Swarm.Language.Types

Associated Types

type U (f t)

Methods

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

fromU :: U (f t) -> Maybe (f t)