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.
-}