Changes since Idris 1

Idris 2 is mostly backwards compatible with Idris 1, with some minor exceptions. This document describes the changes, approximately in order of likelihood of encountering them in practice. New features are described at the end, in Section New features.

The Section Type Driven Development with Idris: Updates Required describes how these changes affect the code in the book Type-Driven Development with Idris by Edwin Brady, available from Manning.

Note

The documentation for Idris has been published under the Creative Commons CC0 License. As such to the extent possible under law, The Idris Community has waived all copyright and related or neighboring rights to Documentation for Idris.

More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

New Core Language: Quantities in Types

Idris 2 is based on Quantitative Type Theory (QTT), a core language developed by Bob Atkey and Conor McBride. In practice, this means that every variable in Idris 2 has a quantity associated with it. A quantity is one of:

• 0, meaning that the variable is erased at run time

• 1, meaning that the variable is used exactly once at run time

• Unrestricted, which is the same behaviour as Idris 1

For more details on this, see Section Multiplicities. In practice, this might cause some Idris 1 programs not to type check in Idris 2 due to attempting to use an argument which is erased at run time.

Erasure

In Idris, names which begin with a lower case letter are automatically bound as implicit arguments in types, for example in the following skeleton definition, n, a and m are implicitly bound:

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs

One of the difficulties in compiling a dependently typed programming language is deciding which arguments are used at run time and which can safely be erased. More importantly, it’s one of the difficulties when programming: how can a programmer know when an argument will be erased?

In Idris 2, a variable’s quantity tells us whether it will be available at run time or not. We can see the quantities of the variables in scope in append_rhs by inspecting the hole at the REPL:

Main> :t append_rhs
 0 m : Nat
 0 a : Type
 0 n : Nat
   ys : Vect m a
   xs : Vect n a
-------------------------------------
append_rhs : Vect (plus n m) a

The 0 next to m, a and n mean that they are in scope, but there will be 0 occurrences at run-time. That is, it is guaranteed that they will be erased at run-time.

This does lead to some potential difficulties when converting Idris 1 programs, if you are using implicit arguments at run time. For example, in Idris 1 you can get the length of a vector as follows:

vlen : Vect n a -> Nat
vlen {n} xs = n

This might seem like a good idea, since it runs in constant time and takes advantage of the type level information, but the trade off is that n has to be available at run time, so at run time we always need the length of the vector to be available if we ever call vlen. Idris 1 can infer whether the length is needed, but there’s no easy way for a programmer to be sure.

In Idris 2, we need to state explicitly that n is needed at run time

vlen : {n : Nat} -> Vect n a -> Nat
vlen xs = n

(Incidentally, also note that in Idris 2, names bound in types are also available in the definition without explicitly rebinding them.)

This also means that when you call vlen, you need the length available. For example, this will give an error

sumLengths : Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen ys

Idris 2 reports:

vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
m is not accessible in this context

This means that it needs to use m as an argument to pass to vlen xs, where it needs to be available at run time, but m is not available in sumLengths because it has multiplicity 0.

We can see this more clearly by replacing the right hand side of sumLengths with a hole…

sumLengths : Vect m a -> Vect n a -> Nat
sumLengths xs ys = ?sumLengths_rhs

…then checking the hole’s type at the REPL:

Main> :t sumLengths_rhs
 0 n : Nat
 0 a : Type
 0 m : Nat
   ys : Vect n a
   xs : Vect m a
-------------------------------------
sumLengths_rhs : Nat

Instead, we need to give bindings for m and n with unrestricted multiplicity

sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen xs

Remember that giving no multiplicity on a binder, as with m and n here, means that the variable has unrestricted usage.

If you’re converting Idris 1 programs to work with Idris 2, this is probably the biggest thing you need to think about. It is important to note, though, that if you have bound implicits, such as…

excitingFn : {t : _} -> Coffee t -> Moonbase t

…then it’s a good idea to make sure t really is needed, or performance might suffer due to the run time building the instance of t unnecessarily!

One final note on erasure: it is an error to try to pattern match on an argument with multiplicity 0, unless its value is inferrable from elsewhere. So, the following definition is rejected

badNot : (0 x : Bool) -> Bool
badNot False = True
badNot True = False

This is rejected with the error:

badnot.idr:2:1--3:1:Attempt to match on erased argument False in
Main.badNot

The following, however, is fine, because in sNot, even though we appear to match on the erased argument x, its value is uniquely inferrable from the type of the second argument

data SBool : Bool -> Type where
     SFalse : SBool False
     STrue  : SBool True

sNot : (0 x : Bool) -> SBool x -> Bool
sNot False SFalse = True
sNot True  STrue  = False

Experience with Idris 2 so far suggests that, most of the time, as long as you’re using unbound implicits in your Idris 1 programs, they will work without much modification in Idris 2. The Idris 2 type checker will point out where you require an unbound implicit argument at run time - sometimes this is both surprising and enlightening!

Linearity

Full details on linear arguments with multiplicity 1 are given in Section Multiplicities. In brief, the intuition behind multiplicity 1 is that if we have a function with a type of the following form…

f : (1 x : a) -> b

…then the guarantee given by the type system is that if f x is used exactly once, then x is used exactly once in the process.

Prelude and base libraries

The Prelude in Idris 1 contained a lot of definitions, many of them rarely necessary. The philosophy in Idris 2 is different. The (rather vaguely specified) rule of thumb is that it should contain the basic functions required by almost any non-trivial program.

This is a vague specification since different programmers will consider different things absolutely necessary, but the result is that it contains:

• Anything the elaborator can desugar to (e.g. tuples, (), =)

• Basic types Bool, Nat, List, Stream, Dec, Maybe, Either

• The most important utility functions: id, the, composition, etc

• Interfaces for arithmetic and implementations for the primitives and basic types

• Basic Char and String manipulation

• Show, Eq, Ord, and implementations for all types in the prelude

• Interfaces and functions for basic proof (cong, Uninhabited, etc)

• Semigroup, Monoid

• Functor, Applicative, Monad and related functions

• Foldable, Alternative and Traversable

• Range, for list range syntax

• Console IO

Anything which doesn’t fit in here has been moved to the base libraries. Among other places, you can find some of the functions which used to be in the prelude in:

• Data.List and Data.Nat

• Data.Maybe and Data.Either

• System.File and System.Directory, (file management was previously part of the prelude)

• Decidable.Equality

Smaller Changes

Ambiguous Name Resolution

Idris 1 worked very hard to resolve ambiguous names, by type, even if this involved some complicated interaction with interface resolution. This could sometimes be the cause of long type checking times. Idris 2 simplifies this, at the cost of sometimes requiring more programmer annotations on ambiguous names.

As a general rule, Idris 2 will be able to disambiguate between names which have different concrete return types (such as data constructors), or which have different concrete argument types (such as record projections). It may struggle to resolve ambiguities if one name requires an interface to be resolved. It will postpone resolution if a name can’t be resolved immediately, but unlike Idris 1, it won’t attempt significant backtracking. If you have deeply nested ambiguous names (beyond a small threshold, default 3) Idris 2 will report an error. You can change this threshold with a directive, for example:

%ambiguity_depth 10

However, in such circumstances it is almost certainly a better idea to disambiguate explicitly.

Indeed in general, if you get an ambiguous name error, the best approach is to give the namespace explicitly. You can also rebind names locally:

Main> let (::) = Prelude.(::) in [1,2,3]
[1, 2, 3]

One difficulty which remains is resolving ambiguous names where one possibility is an interface method, and another is a concrete top level function. For example, we may have:

Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b
LinearIO.(>>=) : (1 act : IO a) -> (1 k : a -> IO b) -> IO b

As a pragmatic choice, if type checking in a context where the more concrete name is valid (LinearIO.(>>=) here, so if type checking an expression known to have type IO t for some t), the more concrete name will be chosen.

This is somehow unsatisfying, so we may revisit this in future!

Modules, namespaces and export

The visibility rules, as controlled by the private, export and public export modifiers, now refer to the visibility of names from other namespaces, rather than other files.

So if you have the following, all in the same file…

namespace A
  private
  aHidden : Int -> Int
  aHidden x = x * 2

  export
  aVisible : Int -> Int
  aVisible x = aHidden x

namespace B
  export
  bVisible : Int -> Int
  bVisible x = aVisible (x * 2)

…then bVisible can access aVisible, but not aHidden.

Records are, as before, defined in their own namespace, but fields are always visible from the parent namespace.

Also, module names must now match the filename in which they’re defined, with the exception of the module Main, which can be defined in a file with any name.

%language pragmas

There are several %language pragmas in Idris 1, which define various experimental extensions. None of these are available in Idris 2, although extensions may be defined in the future.

Also removed was the %access pragma for default visibility, use visibility modifiers on each declaration instead.

let bindings

let bindings, i.e. expressions of the form let x = val in e have slightly different behaviour. Previously, you could rely on the computational behaviour of x in the scope of e, so type checking could take into account that x reduces to val. Unfortunately, this leads to complications with case and with clauses: if we want to preserve the computational behaviour, we would need to make significant changes to the way case and with are elaborated.

So, for simplicity and consistency (and, realistically, because I don’t have enough time to resolve the problem for case and with) the above expression let x = val in e is equivalent to (\x => e) val.

So, let now effectively generalises a complex subexpression. If you do need the computational behaviour of a definition, it is now possible using local function definitions instead - see Section Local function definitions below.

Also, an alternative syntax let x := val in e is available. See Section let bindings for more info.

auto-implicits and Interfaces

Interfaces and auto-implicit arguments are similar, in that they invoke an expression search mechanism to find the value of an argument. In Idris 1, they were implemented separately, but in Idris 2, they use the same mechanism. Consider the following total definition of fromMaybe:

data IsJust : Maybe a -> Type where
     ItIsJust : IsJust (Just val)

fromMaybe : (x : Maybe a) -> {auto p : IsJust x} -> a
fromMaybe (Just x) {p = ItIsJust} = x

Since interface resolution and auto-implicits are now the same thing, the type of fromMaybe can be written as:

fromMaybe : (x : Maybe a) -> IsJust x => a

So now, the constraint arrow => means that the argument will be found by auto-implicit search.

When defining a data type, there are ways to control how auto-implicit search will proceed, by giving options to the data type. For example:

data Elem : (x : a) -> (xs : List a) -> Type where
     [search x]
     Here : Elem x (x :: xs)
     There : Elem x xs -> Elem x (y :: xs)

The search x option means that auto-implicit search for a value of type Elem t ts will start as soon as the type checker has resolved the value t, even if ts is still unknown.

By default, auto-implicit search uses the constructors of a data type as search hints. The noHints option on a data type turns this behaviour off.

You can add your own search hints with the %hint option on a function. For example:

data MyShow : Type -> Type where
     [noHints]
     MkMyShow : (myshow : a -> String) -> MyShow a

%hint
showBool : MyShow Bool
showBool = MkMyShow (\x => if x then "True" else "False")

myShow : MyShow a => a -> String
myShow @{MkMyShow myshow} = myshow

In this case, searching for MyShow Bool will find showBool, as we can see if we try evaluating myShow True at the REPL:

Main> myShow True
"True"

In fact, this is how interfaces are elaborated. However, %hint should be used with care. Too many hints can lead to a large search space!

Record fields

Record fields can now be accessed via a .. For example, if you have:

record Person where
    constructor MkPerson
    firstName, middleName, lastName : String
    age : Int

and you have a record fred : Person, then you can use fred.firstName to access the firstName field.

Totality and Coverage

%default covering is now the default status, so all functions must cover all their inputs unless stated otherwise with a partial annotation, or switching to %default partial (which is not recommended - use a partial annotation instead to have the smallest possible place where functions are partial).

Build artefacts

This is not really a language change, but a change in the way Idris saves checked files, and still useful to know. All checked modules are now saved in a directory build/ttc, in the root of the source tree, with the directory structure following the directory structure of the source. Executables are placed in build/exec.

Packages

Dependencies on other packages are now indicated with the depends field, the pkgs field is no longer recognized. Also, fields with URLS or other string data (other than module or package names), must be enclosed in double quotes. For example:

package lightyear

sourceloc  = "git://git@github.com:ziman/lightyear.git"
bugtracker = "http://www.github.com/ziman/lightyear/issues"

depends = effects

modules = Lightyear
        , Lightyear.Position
        , Lightyear.Core
        , Lightyear.Combinators
        , Lightyear.StringFile
        , Lightyear.Strings
        , Lightyear.Char
        , Lightyear.Testing

New features

As well as the change to the core language to use quantitative type theory, described above, there are several other new features.

Local function definitions

Functions can now be defined locally, using a let block. For example, greet in the following example, which is defined in the scope of a local variable x:

chat : IO ()
chat
    = do putStr "Name: "
         x <- getLine
         let greet : String -> String
             greet msg = msg ++ " " ++ x
         putStrLn (greet "Hello")
         putStrLn (greet "Bye")

These let blocks can be used anywhere (in the middle of do blocks as above, but also in any function, or in type declarations). where blocks are now elaborated by translation into a local let.

However, Idris no longer attempts to infer types for functions defined in where blocks, because this was fragile. This may be reinstated, if we can come up with a good, predictable approach.

Scope of implicit arguments

Implicit arguments in a type are now in scope in the body of a definition. We’ve already seen this above, where n is in scope automatically in the body of vlen:

vlen : {n : Nat} -> Vect n a -> Nat
vlen xs = n

This is important to remember when using where blocks, or local definitions, since the names in scope will also be in scope when declaring the type of the local definition. For example, the following definition, where we attempt to define our own version of Show for Vect, will fail to type check:

showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
  where
    showBody : Vect n a -> String
    showBody [] = ""
    showBody [x] = show x
    showBody (x :: xs) = show x ++ ", " ++ showBody xs

This fails because n is in scope already, from the type of showVect, in the type declaration for showBody, and so the first clause showBody [] will fail to type check because [] has length Z, not n. We can fix this by locally binding n:

showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
  where
    showBody : forall n . Vect n a -> String
    ...

Or, alternatively, using a new name:

showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
  where
    showBody : Vect n' a -> String
    ...

Idris 1 took a different approach here: names which were parameters to data types were in scope, other names were not. The Idris 2 approach is, we hope, more consistent and easier to understand.

Function application syntax additions

From now on you can utilise the new syntax of function applications:

f {x1 [= e1], x2 [= e2], ...}

There are three additions here:

1. More than one argument can be written in braces, separated with commas:

record Dog where
  constructor MkDog
  name : String
  age : Nat

-- Notice that `name` and `age` are explicit arguments.
-- See paragraph (2)
haveADog : Dog
haveADog = MkDog {name = "Max", age = 3}

pairOfStringAndNat : (String, Nat)
pairOfStringAndNat = MkPair {x = "year", y = 2020}

myPlus : (n : Nat) -> (k : Nat) -> Nat
myPlus {n = Z   , k} = k
myPlus {n = S n', k} = S (myPlus n' k)

twoPlusTwoIsFour : myPlus {n = 2, k = 2} === 4
twoPlusTwoIsFour = Refl

2. Arguments in braces can now correspond to explicit, implicit and auto implicit dependent function types (Pi types), provided the domain type is named:

myPointlessFunction : (exp : String) -> {imp : String} -> {auto aut : String} -> String
myPointlessFunction exp = exp ++ imp ++ aut

callIt : String
callIt = myPointlessFunction {imp = "a ", exp = "Just ", aut = "test"}

Order of the arguments doesn’t matter as long as they are in braces and the names are distinct. It is better to stick named arguments in braces at the end of your argument list, because regular unnamed explicit arguments are processed first and take priority:

myPointlessFunction' : (a : String) -> String -> (c : String) -> String
myPointlessFunction' a b c = a ++ b ++ c

badCall : String
badCall = myPointlessFunction' {a = "a", c = "c"} "b"

This snippet won’t type check, because “b” in badCall is passed first, although logically we want it to be second. Idris will tell you that it couldn’t find a spot for a = "a" (because “b” took its place), so the application is ill-formed.

Thus if you want to use the new syntax, it is worth naming your Pi types.

3. Multiple explicit arguments can be “skipped” more easily with the following syntax:

f {x1 [= e1], x2 [= e2], ..., xn [= en], _}

or

f {}

in case none of the named arguments are wanted.

Examples:

import Data.Nat

record Four a b c d where
  constructor MkFour
  x : a
  y : b
  z : c
  w : d

firstTwo : Four a b c d -> (a, b)
firstTwo $ MkFour {x, y, _} = (x, y)
-- firstTwo $ MkFour {x, y, z = _, w = _} = (x, y)

dontCare : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
dontCare {} = plusCommutative {}
--dontCare _ _ _ _ _ = plusCommutative _ _

Last rule worth noting is the case of named applications with repeated argument names, e.g:

data WeirdPair : Type -> Type -> Type where
  MkWeirdPair : (x : a) -> (x : b) -> WeirdPair a b

weirdSnd : WeirdPair a b -> b
--weirdSnd $ MkWeirdPair {x, x} = x
--                        ^
-- Error: "Non linear pattern variable"
-- But that one is okay:
weirdSnd $ MkWeirdPair {x = _, x} = x

In this example the name x is given repeatedly to the Pi types of the data constructor MkWeirdPair. In order to deconstruct the WeirdPair a b in weirdSnd, while writing the left-hand side of the pattern-matching clause in a named manner (via the new syntax), we have to rename the first occurrence of x to any fresh name or the _ as we did. Then the definition type checks normally.

In general, duplicate names are bound sequentially on the left-hand side and must be renamed for the pattern expression to be valid.

The situation is similar on the right-hand side of pattern-matching clauses:

0 TypeOf : a -> Type
TypeOf _ = a

weirdId : {0 a : Type} -> (1 a : a) -> TypeOf a
weirdId a = a

zero : Nat
-- zero = weirdId { a = Z }
--                      ^
-- Error: "Mismatch between: Nat and Type"
-- But this works:
zero = weirdId { a = Nat, a = Z }

Named arguments should be passed sequentially in the order they were defined in the Pi types, regardless of their (imp)explicitness.

Better inference

In Idris 1, holes (that is, unification variables arising from implicit arguments) were local to an expression, and if they were not resolved while checking the expression, they would not be resolved at all. In Idris 2, they are global, so inference works better. For example, we can now say:

test : Vect ? Int
test = [1,2,3,4]

Main> :t test
Main.test : Vect (S (S (S (S Z)))) Int

The ?, incidentally, differs from _ in that _ will be bound as an implicit argument if unresolved after checking the type of test, but ? will be left as a hole to be resolved later. Otherwise, they can be used interchangeably.

Dependent case

case blocks were available in Idris 1, but with some restrictions. Having better inference means that case blocks work more effectively in Idris 2, and dependent case analysis is supported.

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys
    = case xs of
           [] => ys
           (x :: xs) => x :: append xs ys

The implicit arguments and original values are still available in the body of the case. Somewhat contrived, but the following is valid:

info : {n : _} -> Vect n a -> (Vect n a, Nat)
info xs
    = case xs of
           [] => (xs, n)
           (y :: ys) => (xs, n)

Record updates

Dependent record updates work, provided that all relevant fields are updated at the same time. Dependent record update is implemented via dependent case blocks rather than by generating a specific update function for each field as in Idris 1, so you will no longer get mystifying errors when trying to update dependent records!

For example, we can wrap a vector in a record, with an explicit length field:

record WrapVect a where
  constructor MkVect
  purpose : String
  length : Nat
  content : Vect length a

Then, we can safely update the content, provided we update the length correspondingly:

addEntry : String -> WrapVect String -> WrapVect String
addEntry val = { length $= S,
                 content $= (val :: ) }

Another novelty - new update syntax (previous one still functional):

record Three a b c where
  constructor MkThree
  x : a
  y : b
  z : c

-- Yet another contrived example
mapSetMap : Three a b c -> (a -> a') -> b' -> (c -> c') -> Three a' b' c'
mapSetMap three@(MkThree x y z) f y' g = {x $= f, y := y', z $= g} three

The record keyword has been discarded for brevity, symbol := replaces = in order to not introduce any ambiguity.

Generate definition

A new feature of the IDE protocol supports generating complete definitions from a type signature. You can try this at the REPL, for example, given our favourite introductory example…

append : Vect n a -> Vect m a -> Vect (n + m) a

…assuming this is defined on line 3, you can use the :gd command as follows:

Main> :gd 3 append
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

This works by a fairly simple brute force search, which tries searching for a valid right hand side, and case splitting on the left if that fails, but is remarkably effective in a lot of situations. Some other examples which work:

my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
my_curry : ((a, b) -> c) -> a -> b -> c
my_uncurry : (a -> b -> c) -> (a, b) -> c
append : Vect n a -> Vect m a -> Vect (n + m) a
lappend : (1 xs : List a) -> (1 ys : List a) -> List a
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

This is available in the IDE protocol via the generate-def command.

Chez Scheme target

The default code generator is, for the moment, Chez Scheme. Racket and Gambit code generators are also available. Like Idris 1, Idris 2 supports plug-in code generation to allow you to write a back end for the platform of your choice. To change the code generator, you can use the :set cg command:

Main> :set cg racket

Early experience shows that both are much faster than the Idris 1 C code generator, in both compile time and execution time (but we haven’t done any formal study on this yet, so it’s just anecdotal evidence).