Alexander Kuklev (akuklev) wrote,
Alexander Kuklev

Notational sketch (Linear Dependent Type Theory)

If we restrict simply typed lambda calculus by forbidding anonymous cloning and discarding values, we'll obtain a computational content of minimal intuitionistic linear logic. Unfortunatelly it's very trivial, unless we add some type formers along with their constructors and destructors. Pure simply typed lambda calculus only has atomic types, function types (A -o B), Zero type and Unit type.

First of all let's extend this calculus by several type formers:
# The usual ones:
(A, B) # pair, (multiplicative) product of A and B
Either(A, B) # disjoint sum, (additive) sum of A and B

# The unusual ones:
Choose(A, B) # the user may choose to take A or B from the box.
Superposition(A, B) # the user must uniformly transform both A and B

(The last one is very much like Either(A, B) except the user cannot get to know which one of the cases really occurs: in some models Superposition(A, B) encodes quantum superpositions of objects. The Schrödinger cat is Superposition(LivingCat, DeadCat) as long as the box is closed and becomes Either(LivingCat, DeadCat) in the context of observer who opened the box. In game/resource semantics it's simply the pair with delayed choice.)

Intuitionistic types
First of all, let's give a way how to restore usual intuitionistic types. Intuitionistic type or ValueType is a type T equipped with structure of symmetric comonoid (with comultiplication clone : T -o (T, T) and counit discard : T -o Unit). On such types we can define usual lambda terms (x : X) -> Y that use the variable x any finite number of times: these lambda-terms can be rewritten into linear ones using clone and discard operations on X, the symmetry of comonoid X is precisely the property that all such interpretations (i.e. all possible combinations and permutations of clonings and discardings yielding the same number of copies) produce (up to coherent equivalence)equal results. By A -> B (where A is a symmetric comonoid and B any type) we'll denote the type of usual lambda terms taking values of A and producing Bs.

We can also see that pairs (A, B) and disjoint sums Either(A, B) of value types are naturally value types as well. We also want all types without destructors (in particular, universes) to be value types as well, then we can define dependent sums and products (x : X, Y(x)), (x : X) -> Y(x), as long as X is a value type and Y : X -> Type.

In order to proceed do Id-types and type families we'll need to add the value type former Ghost(T) with constructor ⧘_⧙ : T -> Ghost(T) and no destructors guaranteing that all functions depending on Ghost types use their value only as indices and are parametric in these. Now it would probably be not contradictory to require existence of inductive type families indexed by ghost types and universes, perhaps even with any value types. And for any type T there should be a natural Id type _=_ : (x : Ghost(T), t : Ghost(T)) -> Type

This type should be automatically equipped with a structure of a "weak Groupoid", i.e. weak partial Hopf algebra, so its elements are allowed to be cloned, but cloning is not necessary symmetric, only coassociative up to coherent equivalence.

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.