This sort of thing (if I understand the abstracts correctly) can also be done with dependent types: https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/a

This sort of thing (if I understand the abstracts correctly) can also be done with dependent types: https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/a.... This paper was my introduction to dependent typing, so if you have a little Haskell background, you should be able to grok its gist too.