Implicit.agda

-- This module introduces implicit arguments.

module Introduction.Implicit where

-- In Agda you can omit things that the type checker can figure out for itself.
-- This is a crucial feature in a monomorphic language, since you would
-- otherwise be overwhelmed by type arguments.

-- Let's revisit the identity function from 'Introduction.Basics'.

id' : (A : Set) -> A -> A
id' A x = x

-- Since Agda is monomorphic we have to take the type A as an argument. So when
-- using the identity function we have to provide the type explicitly.

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

one : Nat
one = id' Nat (suc zero)

-- Always having to provide the type argument to the identity function would of
-- course be very tedious, and seemingly unnecessary. We would expect the type
-- checker to be able to figure out what it should be by looking at the second
-- argument. And indeed the type checker can do this.

-- One way of indicating that the type checker will have figure something out
-- for itself is to write an underscore (_) instead of the term. So when
-- applying the identity function we can write

two : Nat
two = id' _ (suc one)

-- Now the type checker will try to figure out what the _ should be, and in
-- this case it will have no problems doing so. If it should fail to infer the
-- value of an _ it will issue an error message.

-- In the case of the identity function we expect the type argument to always
-- be inferrable so it would be nice if we could avoid having to write the _.
-- This can be achieved by declaring the first argument as an implicit
-- argument.

id : {A : Set} -> A -> A        -- implicit arguments are enclosed in curly braces
id x = x  -- now we don't have to mention A in the left-hand side

three : Nat
three = id (suc two)

-- If, for some reason, an implicit argument cannot be inferred it can be given
-- explicitly by enclosing it in curly braces : 

four : Nat
four = id {Nat} (suc three)

-- To summarise we give a bunch of possible variants of the identity function
-- and its use.

-- Various definitions of the identity function. Definitions 0 through 3 are
-- all equivalent, as are definitions 4 through 6.

id0 : (A : Set) -> A -> A
id0 A x = x

id1 : (A : Set) -> A -> A
id1 _ x = x     -- in left-hand sides _ means "don't care"

id2 : (A : Set) -> A -> A
id2 = \A x -> x

id3 = \(A : Set)(x : A) -> x  -- the type signature can be omitted for definitions
                          -- of the form x = e if the type of e can be
                          -- inferred.

id4 : {A : Set} -> A -> A
id4 x = x

id5 : {A : Set} -> A -> A
id5 {A} x = x

id6 : {A : Set} -> A -> A
id6 = \x -> x

id7 = \{A : Set}(x : A) -> x

-- id8 : {A : Set} -> A -> A
-- id8 = \{A} x -> x        -- this doesn't work since the type checker assumes
                            -- that the implicit A has been has been omitted in
                            -- the left-hand side (as in id6).

-- Various uses of the identity function.
zero0 = id0 Nat zero
zero1 = id0 _   zero  -- in right-hand sides _ means "go figure"

zero2 = id4       zero
zero3 = id4 {Nat} zero
zero4 = id4 {_}   zero  -- This is equivalent to zero2, but it can be useful if
                        -- a function has two implicit arguments and you need
                        -- to provide the second one (when you provide an
                        -- implicit argument explicitly it is assumed to be the
                        -- left-most one).

-- In this module we have looked at implicit arguments as a substitute for
-- polymorphism. The implicit argument mechanism is more general than that and
-- not limited to inferring the values of type arguments. For more information
-- on implicit arguments see, for instance
--  'Introduction.Data.ByRecursion'