2
$\begingroup$

The "function" type $\rightarrow$ is predefined in Agda. But how would one define it if it was not predefined? Specifically I am talking about $\rightarrow$ in:

data Nat : Set where
     zero : Nat
     Suc : Nat -> Nat
$\endgroup$
2
$\begingroup$

It is not possible: -> is built into the underlying logic of Agda (and most dependently typed languages).

In particular, -> is not a type constructor, because it has binding properties. Because you can define things like (n : Nat) -> Vec A n, the compiler needs to add n to the variables in scope in the right hand side of the arrow, so this can't be done.

There are ways to cheat with bindings. For example, you can define $\exists x : T \ldotp S[x]$ as ex T (\x -> S), i.e. using a lambda to represent the binding. But, that lambda is typed using ->. Having dependent functions built in is the starter that bootstraps the rest of the type system. It's the only way the language can express quantification, so it ends up being critical.

$\endgroup$
  • $\begingroup$ So you mean we can not have some definition like "data _ -> _ (A,B : Set) : Set_2 where ..."? Does that mean inductive type is kind of a bootstrap for intuitionistic type theory and different than other connectives like sum and product type? $\endgroup$ – K. Smith Nov 15 '17 at 23:02
  • $\begingroup$ Exactly. How would you even write the constructors of an inductive type if the arrow wasn't already given? $\endgroup$ – jmite Nov 16 '17 at 8:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.