Overview

Here you will find an overview of typed: a library devoted to allow type safe constructions in Python.

1. Overview: Types

2. Overview: Relations

3. Overview: Parametric Types

4. Overview: Dependent Types

5. Overview: Models

6. Other Docs

Overview: Types

The typed library introduces a new type system for Python. Everything begins with universes. These creates universal metatypes, which extends abstract metatype. These, in turn, create types, as follows:

          creates              extends              creates
UNIVERSE ────────>  UNIVERSAL ─────────> ABSTRACT  ─────────> TYPES
                    METATYPES            METATYPES

The typed type system is generated by a single universe, denoted by __UNIVERSE__, and by a single universal metatype, denoted by _TYPE_. So, every abstract metatype is a subclass of _TYPE_. In turn, _TYPE_ creates a special type TYPE of which any other type is an object.

Notation.

1. abstract metatypes are denoted in UPPERCASE

2. types are denoted in CamelCase.

What characterize an entity in the typed type system is their objects. We check if a symbol x is an object of an entity Entity with the expression x in Entity. Thus, for example, a symbol SomeType is a type precisely if SomeType in TYPE.

Every Python builtin type has an incarnation as a typed type, which is created by a specific abstract metatype:

Python builtin	typed type	metatype
type(None)	Nill	NILL
bool	Bool	BOOL
int	Int	INT
float	Float	FLOAT
str	Str	STR
…

table 1: python types _vs_ typed types

Overview: Relations

The entities in the typed type system can be related in different ways. The basic way is in terms of a typed function, which are callable entities. This is a function whose parameters have type annotations which are checked at runtime. They form a type Typed, of which the other type relations are subtypes, forming the following hierarchy:

                               extends
          extends            ┌────────> Operation
        ┌────────> Factory ──┤
Typed ──┤                    └────────> Dependent
        └────────> Condition   extends
         extends

1. A type factory is a typed function that constructs a type, hence that take values into TYPE.

2. In turn, a condition (a.k.a predicate) is a typed function that returns a boolean, i.e., that take values into Bool.

3. A type operation is a type factory such that all type annotations are subtypes of TYPE.

4. A dependent type is a special type factory with the attribute .is_dependent_type set to True.

To each kind of relation there corresponds a decorator which should be used to create such a relation:

relation	decorator
Typed	@typed
Factory	@factory
Condition	@condition
Operation	@operation
Dependent	@dependent

table 2: relations and decorators

Overview: Parametric Types

In typed there are special mixed entities, which are both types and type relations (more precisely, type factories or type operations). These are the so-called parametric types.

An example is Typed. It is the type of all typed functions. It is also a type operation: it can receive a tuple of types (SomeType, OtherType, ...) and another type ReturnType, returning the subtype Typed(SomeType, OtherType, ..., cod=ReturnType) of Typed of all typed functions whose domain is (SomeType, OtherType, ...) and whose codomain is ReturnType.

Overview: Dependent Types

In a type system, dependent types are crucially important to provide a strong type expressiveness needed to ensure type safety. In typed they are implemented as type factories and can be passed as type annotations to any typed function.

This means that in typed one may have a relation between types such that the type of a parameter depends on the value of the other parameters.

Overview: Models

One can say that a type system presents type safety when each validation is realized as a type checking. This include data validation. Data, in turn, is typically presented in terms of hierarchical structure, as JSON.

In typed one can deal with data validation by constructing parameterized subtypes of a Json type known as models. These are constructed from certain type factories known as model factories. Different model factories constructs models with different kinds of validation and are constructed from specific abstract metatypes.

model factory	description	metatype
Model	basic validation	MODEL
Exact	exact validation	EXACT
Ordered	order validation	ORDERED
Rigid	order and exact validation	RIGID

table 3: model factories

Other Docs

1. types

2. models

3. errors

4. examples

5. api

6. glossary

7. changelog