Write function type on multiple lines in Idris

Question

How do I split a type declaration into multiple lines in Idris? Types should drive development. So they may become quite long and not fit on screen. Like this one:

addMatrices : (augent : Vect rowCount (Vect columnCount element)) -> (addend: Vect rowCount (Vect columnCount element)) -> Vect rowCount (Vect columnCount element)

I don't know Idris, but you can probably make a new type (or an alias, if idris allows it) like Matrix Nat Nat Set, which will reduce your declaration by some amount. — Al.G.
Al.G. Thank you for proposing your solutuion. I'll try to find out more about aliases in Idris. — Alexander Novikov

joel joel · Accepted Answer · 2020-06-29T17:51:44

To do it with formatting only, you can do it as you've done,

addMatrices : (augent : Vect rowCount (Vect columnCount element)) -> 
              (addend: Vect rowCount (Vect columnCount element)) -> 
              Vect rowCount (Vect columnCount element)

The docs say

New declarations must begin at the same level of indentation as the preceding declaration.

Similarly, the book only says, in Section 2.4.1 Whitespace significance: the layout rule,

... in any list of definitions and declarations, all must begin in precisely the same column.

Since the new line isn't a new declaration, I take this to mean the new line can start at any level of indentation, so

addMatrices : (augent : Vect rowCount (Vect columnCount element)) -> 
       (addend: Vect rowCount (Vect columnCount element)) -> 
          Vect rowCount (Vect columnCount element)

and other variants would also be valid.

Alternatively, following on from Al.G.'s comment, you can use a type alias, but if rowCount and columnCount aren't in scope, which I'm guessing they aren't for you, you'll need a type-level function, which is a generalisation of a type alias. It's a function that returns a type.

Matrix : Nat -> Nat -> Type -> Type
Matrix rows cols elem = Vect rows (Vect cols elem)

Then you'll have

addMatrices : (augent : Matrix rowCount columnCount element) -> 
              (addend: Matrix rowCount columnCount element) -> 
              Matrix rowCount columnCount element

which isn't much shorter.

To be honest, I'd look at using shorter names and take advantage of any obvious context

addMatrices : (augent : Vect r (Vect c elem)) -> (addend: Vect r (Vect c elem)) -> Vect r (Vect c elem)

Write function type on multiple lines in Idris

2 Answers