-- 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'