3.8. Local Definitions

It is possible to write terms with local definitions. There is a let form and a where form.

1 + f 10 where
    f x := 2 * g x                      -- inside out
    g x := x + 100

let g x := x + 100                      -- outside in
    f x := 2 * g x
:=
    1 + f 10

-- The same with fully elaborated definitions
1 + f 10 where
    f (x: Int): Int := 2 * g x
    g (x: Int): Int := x + 100

let
    g (x: Int): Int := x + 100
    f (x: Int): Int := 2 * g x
:=
    1 + f 10

A local definition has the same syntax as the global definition of a function / constant. However the compiler has more context information, because the locally defined symbol is used in the main expression. Therefore the compiler can infer from the main expression typing information which need not be given by the user in the local declaration.

The where form and the let form are fully equivalent. where works inside out i.e. an inner (i.e. previous) definition can use outer definitions. let works outside in i.e. outer (i.e. previous) definitions can be used by inner definitions.

Choosing between both forms is a matter of taste. In many cases the where form is preferable because it is more goal driven. You first write your main expression with some unknowns and then you define successively the unknowns in an inside out manner.

Like in pattern match expressions, implicit arguments can be ommitted as long as the compiler can infer them from the usage. But for reasons of elaboration we insist that implicit arguments are either not mentioned or all are mentioned in the corresponding local definition.

The handling of implicit arguments is a subtle difference between local and global definitions. Since there is no usage context in global definitions, all implicit arguments must be mentioned in the definition. Their types might be inferrable, but they must be mentioned. In local definitions the compiler might be able to infer from the usage the type of a local definition. Having the type information, it is clear that and where there are implicit arguments.