CODEWITHSUNDEEP
typescoqdependent-type
Zhangsheng
Zhangsheng

Reputation: 85

Dependent type indexed by a term of its own type

Dependent types are types which depend on a term of a type. So I'm wondering if it is possible for a dependent type to be indexed by a term of its own type? What I have tried is this which

Parameter Obj: Type.
Parameter a: Obj.
Parameter foo: Obj -> Type. 
Parameter b : foo a.
Parameter boo : Obj -> Type.
Fail Parameter c : boo b.

fails since The term "b" has type "foo a" while it is expected to have type "Obj".. Is what I'm trying to do possible with dependent type theory and how do I implement it with Coq?

Upvotes: 2

Views: 81

Answers (1)

András Kovács
András Kovács

Reputation: 30103

It's not directly possible in any system that I know of. It works indirectly in Agda, but does not work in any way in Coq. In Agda, you need to wrap the index with a different type:

-- forward declaration
data A : Set
data B : A -> Set

data A where
  wrap : B -> A

data B where
  -- list your other constructors here

This form of indexing (called "inductive-inductive") is not yet supported by Coq.

Upvotes: 2

Related Questions