Idris Language - Let and Where

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.

The where binding is usually used for functions.


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)


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


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
x = 1
y = 1

metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.