New answers tagged type-theory
3
We certainly do not need very many $W$-types.
If we also have universes, we only need one $W$-type, namely the natural numbers. For example, the UniMath library uses just the natural numbers and no other inductive types (if we discount the fact that standard types constructors, such as products and sum, are defined inductively in Coq).
2
You asked several questions.
You asked about a type indexed by a list, so you can do this.
data DataType (A : Type) (F : A -> Type) : List A -> Type where
empty : DataType A F []
_bla_ : forall {xs} {x} -> DataType A F xs -> F x -> DataType A F (x ∷ xs)
Where F is a type family that is indexed by the elements of the list.
Apart from that, ...
0
You can define an auxiliary predicate x ∈ ℓ whose elements are all the positions in ℓ at which x appears. With that in hand, you can do it as follows:
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
infixr 5 _::_
infix 4 _∈_
data _∈_ {A} (x : A) : List A → Set where
∈-head : ∀ {ℓ} → x ∈ x :: ℓ
∈-tail : ∀ {y} {ℓ} → x ∈ ℓ → x ∈ ...
5
Uniqueness is not converse to introduction. Uniqueness rules in type theory are
components of isomorphisms. If a type former is specified with an isomorphism, then
Constructors form one map
Eliminators form the inverse map
β-rules express elim ∘ con = id
η-rules (uniqueness) express con ∘ elim = id
For example, function types are given as Tm Γ (Π A B) ≃ Tm ...
2
Generally, there will be one context-free grammar for both types and terms, and judgements will be used to identify those expressions which are types and which expressions are terms of a particular type.
This has been written down many, many times. For a pretty typical example, you could look at Abel, Coquand and Dybjer's LICS 2007 paper, Normalization by ...
0
Generally, HM type inference should be a part of the I/O interface, far away from the inference kernel. This constraint will drive your design to ensure that this won't be a problem. In your $\mathrm{reflexive}$ example, there are two polymorphic constants at play:
$$\mathrm{reflexive} : (\alpha \to \alpha \to \mathrm{bool}) \to \mathrm{bool}$$
$$(=) : \...
Top 50 recent answers are included
