module List where
{-
Data types can be polymorphic too. For example, in Haskell we have the type [X] of lists where the elements belong to the type X for an arbitrary type X. In Agda we declare the polymorphic data type of list as follows:
-}
data List (A : Set) : Set where
[] : List A
_::_ : A -> List A -> List A
{-
This declaration states that the type of List is Set → Set: if A : Set then List A : Set. Moreover, the types of the constructors have an implicit argument, which is not written out in the declaration above. Their proper types are:
[] : {A : Set} -> List A
_::_ : {A : Set} -> A -> List A -> List A
Let us now define some list functions, for example map is defined as follows:
-}
map : {A B : Set} -> (A -> B) -> List A -> List B
map f [] = []
map f (a :: as) = f a :: map f as
{-
Agda is a language of total functions
-------------------------------------
What about head? Let us try to define
head : {A : Set} → List A -> A
head [] = ?
head (a :: as) = a
In Haskell we can simply define head as a partial function, which is not defined for []. This is not possible in Agda, where all functions are total. The way out would be to define head [] as an explicit error element, for example "Nothing" in Haskell's Maybe type defined by
data Maybe a = Just a | Nothing
Exercise: Define the Maybe type in Agda and the function
head : {A : Set} → List A -> Maybe A
Note that we can make tail total without using Maybe by conventionally defining tail [] = [].
-}