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