A look at Agda's module system

Published: May 12, 2021, 10 a.m.

b'

Agda's module system (beautifully described here) could be seen as intermediate between Haskell's and Standard ML's.\\xa0 It supports nested parametrized modules with information hiding, but does not go all the way to higher-order functors (as in Standard ML).

'