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 Agda is a language of total functions ------------------------------------- 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 {- 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 [] = []. -}