[alduin32]

Oh right, the output is parametrized by the input. I suppose this is what dependent types are.

That's really awesome. Thanks for the explanation.

[masklinn]

> Oh right, the output is parametrized by the input. I suppose this is what dependent types are.

Dependent types is really about the ability to parameterise types over values, and reason on those values-dependent types.