Idris has two different types of binding: let and where. These can be used where there is an expression. At the top level, this is on the right hand side of a function definition.
- A let binding binds a name to an expression, this is before the expression using this syntax:
let x = <expression> in <some expression containing x> - A where binding binds a name to a value, this is after the expression using this syntax:
<some expression containing x> where x=<value>
The where binding is usually used for functions.
Let
A let binding is an expression and binds anywhere in its body. For example the following let binding declares x and y in the expression x+y.
f = let x = 1; y = 2 in (x+y)
Shadowing
This binding is just an assignment of a name to an expression. It is not to be thought of as 'putting some value in a box' as with an assignment in an imperative language.
We can still reuse a variable name, in the same scope, this does not replace the previous binding but it hides it for subsequent uses of the name.
x = 1
x = 2
Where
A where binding is a top level syntax construct (i.e. not an expression) that binds variables at the end of a function. For example the following binds x and y in the function body of f which is x+y.
f = x+y where x=1; y=1
Where clauses following the Haskell layout rule where definitions can be listed on newlines so long as the definitions have greater indentation than the first top level definition they are bound to.
f = x+y
where
x = 1
y = 1
