Dependent Types in Eta
This example demonstrates how you can work with dependent types in Eta via the
singletons library. It shows an example of type-safe matrix multiplication.
To run the program, execute the following in this example's directory:
> etlas install --dependencies-only > etlas run matrix-ex -- 1 2 3 4 Matrices of incompatible size. > etlas run matrix-ex -- 1 2 3 4 ( 8 16 24 32 )
If you had trouble with this tutorial, you can give us feedback by: