<p>Agda's module system (beautifully described <a href='https://agda.readthedocs.io/en/v2.6.0.1/language/module-system.html'>here</a>) could be seen as intermediate between Haskell's and Standard ML's.  It supports nested parametrized modules with information hiding, but does not go all the way to higher-order functors (as in Standard ML).</p>

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

<p>Agda's module system (beautifully described <a href="https://agda.readthedocs.io/en/v2.6.0.1/language/module-system.html" rel="noopener noreferrer">here</a>) could be seen as intermediate between Haskell's and Standard ML's.&nbsp; It supports nested parametrized modules with information hiding, but does not go all the way to higher-order functors (as in Standard ML).</p>

A look at Agda's module system

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Share A look at Agda's module system

Sign up to save your podcasts

A look at Agda's module system

A look at Agda's module system