mirror of
https://github.com/polarity-lang/polarity.git
synced 2025-12-23 09:19:50 +00:00
c786a6704f
* Add CST and parsing for infix declarations * Add infix declarations to symbol table * Add Infix decls to ast * Make testsuite run through again * Implement infix declarations * Validate binding structure of infix decls * Generate docs * Add testcases * Make tests run through again * Add checking of infix declarations * Add testcases * Check that RHS is defined * Fix clippy hints * Add hover information * Add infix to syntax of web editor --------- Co-authored-by: Tim Süberkrüb <dev@timsueberkrueb.io>
100 lines
3.3 KiB
Text
100 lines
3.3 KiB
Text
//
|
||
//
|
||
// Strong Existentials Demystified
|
||
//
|
||
//
|
||
|
||
// In this short development we show that the difference between weak and
|
||
// strong existentials (and similarly between weak and strong Sigma types)
|
||
// corresponds exactly to the two different ways in which products can be
|
||
// polarized: either positively as a data type, or negatively as a codata
|
||
// type. This helps to further demystify their difference, and furthermore
|
||
// gives more evidence that the `self` parameter introduced into our system
|
||
// is justified, since it is necessary for the Existential and Sigma type.
|
||
|
||
//
|
||
// Ordinary product types
|
||
//
|
||
|
||
// Let us start with the simplest case of products, namely non-dependent
|
||
// products `A × B` consisting of an element of type `A` and an element
|
||
// of type `B`. As a datatype it can be written as follows:
|
||
|
||
data Tensor(A B: Type) {
|
||
Sum(A B: Type, x: A, y: B): Tensor(A,B),
|
||
}
|
||
|
||
// Using the negative polarization, the product is specified using the two
|
||
// projections on the first and second element:
|
||
|
||
codata With(A B: Type) {
|
||
With(A,B).π₁(A B: Type): A,
|
||
With(A,B).π₂(A B: Type): B,
|
||
}
|
||
|
||
//
|
||
// Weak and Strong Existentials
|
||
//
|
||
|
||
// Let us now generalize this example to existentials `∃X.T`. In our system,
|
||
// such existentials are represented as `∃(\X. T)`, i.e. the type constructor
|
||
// `∃` takes as argument a function of type `Type -> Type`. We therefore have
|
||
// to introduce the type of functions first:
|
||
|
||
codata Fun(A B: Type) {
|
||
Fun(A,B).ap(A B: Type, x: A): B,
|
||
}
|
||
|
||
infix _ -> _ := Fun(_,_)
|
||
|
||
|
||
// The existential type can be represented using a data type with one constructor
|
||
// `ExistsSum`. This constructor takes as arguments the function `T` of type `Type -> Type`,
|
||
// a type `A` and a witness `W` of type `T.ap(Type,Type,A)` which corresponds to `T[A/X]`
|
||
// in more standard notation.
|
||
|
||
data ExistsPos(T: Type -> Type) {
|
||
ExistsSum(T: Type -> Type, A: Type, W: T.ap(Type,Type,A)): ExistsPos(T),
|
||
}
|
||
|
||
// As a codata type, we still have two projections `eπ₁`and `eπ₂` as in the case
|
||
// of non-dependent products. But the second projection now uses the self-parameter
|
||
// to guarantee that an element of type `T[self.eπ₁/X]` is returned.
|
||
|
||
codata ExistsNeg(T: Type -> Type) {
|
||
ExistsNeg(T).eπ₁(T: Type -> Type): Type,
|
||
(self: ExistsNeg(T)).eπ₂(T: Type -> Type): T.ap(Type,Type, self.eπ₁(T)),
|
||
}
|
||
|
||
//
|
||
// Weak and Strong Sigma Types
|
||
//
|
||
|
||
// Finally, we can consider the case of weak and strong Sigma types, which can
|
||
// now be seen to be nothing more than the difference between a Sigma type defined
|
||
// as a data type vs a codata type. This example is very similar to the case of
|
||
// existentials, except that the type constructor `Σ` is now indexed over both a
|
||
// type `A` and a type family `T: A -> Type`.
|
||
|
||
data ΣPos(A: Type, T: A -> Type) {
|
||
ΣSum(A: Type, T: A -> Type, x: A, w: T.ap(A,Type,x)): ΣPos(A,T),
|
||
}
|
||
|
||
def ΣPos(A,T).defπ₁(A: Type, T: A -> Type): A {
|
||
ΣSum(_,_,x,_) => x,
|
||
}
|
||
|
||
def (self: ΣPos(A,T)).defπ₂(A: Type, T: A -> Type): T.ap(A,Type,self.defπ₁(A,T)) {
|
||
ΣSum(_,_,_,w) => w,
|
||
}
|
||
|
||
|
||
codata ΣNeg(A: Type, T: A -> Type) {
|
||
ΣNeg(A,T).sπ₁(A: Type, T: A -> Type): A,
|
||
(self: ΣNeg(A,T)).sπ₂(A: Type, T: A -> Type): T.ap(A,Type, self.sπ₁(A,T)),
|
||
}
|
||
|
||
codef DefΣSum(A: Type, T: A -> Type, x: A, w: T.ap(A, Type, x)): ΣNeg(A,T) {
|
||
.sπ₁(_,_) => x,
|
||
.sπ₂(_,_) => w,
|
||
}
|