3 ms·
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.
by alduin32 5y ago
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 5y ago> 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.