module LF where
{-
The core of Agda is a lambda calculus with dependent types, often called the "Logical Framework" ("LF"). We already saw that it has a type
"Set" and you can declare data types to be members of this type. So "Set is a type of data types. We do not have
Set : Set
because this would result in a logical paradox, similar to Russell's paradox for naive set theory.
First, we point out that we have the rule that if A : Set, then A is a type, that is, it can stand to the right of the ":"-sign.
Moreover, we do not only have ordinary function types A → B, but also "dependent function types" (x : A) → B, where the type B may depend on the variable x : A.
We shall now see a first example of how such dependent function types can be used, by showing how to express polymorphism. Let us take the simplest possible example: the polymorphic identity combinator would be defined by
-}
I : (X : Set) → X → X
I X x = x
{-
Informally, this says "for any type X, we get a function I X : X → X". Note that this is different from polymorphism in Haskell where we have a function I of type X → X, for a type variable X, and that X does not appear as an argument of I. Note also that the type expression
(X : Set) → X → X
is well-formed, because of what we said above, and that X → X is a type which "depends" on the variable X : Set.
Remark: we can also use λ-notation in Agda and instead write
I = λ X x → x
Implicit arguments
------------------
It would be tedious to always have to write out all type-variable arguments. For this purpose Agda also has facility for declaring arguments to be "implicit" by using the "implicit dependent function type" {x : A} → B. The typing rule is that if b : {x : A} → B, and a : A, then b : B[x := a], that is, that b is a term of type B where the term a has been substituted for the variable x. In this way we can recover Haskell's notation for polymorphism, e g, the type of the identity function with implicit polymorphism is
-}
I-implicit : {X : Set} → X → X
I-implicit x = x
{-
Exercise: write I-implicit using λ-notation!
We can define many polymorphic combinators with implicit arguments. For example, the infix composition combinator can be defined by
-}
_∘_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
(g ∘ f) x = g (f x)
{-
Exercise: Define the K and S-combinators! (See wikipedia if you don't know their definitions.)
In combinatory logic one shows that the two combinators K and S suffice for defining all other combinators. In particular one can show that the identity combinator can be defined as I = S K K. Check what happens if you let Agda normalize S K K! Explain.
-}