About

This documentation contains the definition of the main concepts introduced in typed. They are present in logic ordering.

Concepts

universe.

The typed universe is the class __UNIVERSE__ that works as the metaclass for all abstract metatypes. It requires the implementation of a __instancecheck__ method. Also, it provides a __contains__ method which is implemented precisely by the given __instancecheck__.

universal metatype.

A universal metatype is a Python {lib:class} that has the __UNIVERSE__ as metaclass. The canonical example is _TYPE_: the universal metatype which is the {py:abstract metatype} of the concrete metatype TYPE of all types.

abstract metatype.

An abstract metatype is a Python class which is a subclass of a universal metatype. They are named in uppercase: SOME_META, OTHER_META, …

type.

A type is a class that has an abstract metatype as a metaclass. Types are names in CamelCase: SomeType, OtherType, …

object.

An object of a type is an instance of some type. Thus, x is an object of a type SomeType iff isinstance(x, SomeType) is True. Equivalently, iff x in SomeType is True.

concrete metatype.

A concrete metatype is a type SomeType whose objects are themselves types. There is the concrete metatype TYPE of all types.

subtype.

A type SomeType is a subtype of another type OtherType if, as a class it is a subclass of OtherType.

domain hinted function.

A domain hinted function is a function such that every parameter has a type annotation. They form a type DomHinted.

codomain hinted function.

A codomain hinted function is a function whose return have a type annotation. They form a type CodHinted.

hinted function.

A hinted function is a function which is both domain hinted and codomain hinted. There is the type Hinted of all hinted functions. It is a subtype of both DomHinted and CodHinted.

domain.

The domain of a domain hinted function is the tuple of the type annotations of their parameters.

codomain.

The codomain of a codomain hinted function is its return type annotations.

domain typed function.

A domain typed function is a domain hinted function whose type annotations are types or dependent types which are checked at runtime. They form a type DomTyped which is a subtype of DomHinted.

codomain typed function.

A codomain typed function is a codomain hinted function whose return type annotation is a type or a dependent type, checked at runtime. They form a type CodTyped which is a subtype of CodHinted.

typed function.

A typed function is a function which is both domain hinted and codomain hinted, so that all their type annotations are types or dependent types, being checked at runtime. There is the type Typed of all typed functions. It is a subtype of both DomTyped, CodTyped and Hinted.

type factory.

A type factory is a typed function whose codomain is TYPE, the concrete metatype of all types. Thus, a type factory is some process constructing a type depending on certain parameters.

parametric type.

A parametric type is type which also is a type factory. Thus, it is a type whose abstract metatype has a __call__ method that returns a type factory.

dependent type.

A dependent type is type which also is a type factory. Thus, it is a type whose abstract metatype has a __call__ method that returns a type factory.

condition.

A condition (a.k.a predicate) is a type factory that constructs booleans, hence that take values into Bool.