[<<][haskell][>>][..]
Wed May 8 08:04:02 EDT 2019

Constraining ranges

I have a function (i->s) -> (i'->s), where i is an integer in 0..n,
and i' is in 0..n+1

How to express that in a type?

Probably type families?

Droppig the s, i.e. i->i' becomes something like i -> S i, where S is
the successor type.


https://en.wikipedia.org/wiki/Type_family
https://wiki.haskell.org/GHC/Type_families


EDIT: Type families are type-indexed types.
I want value-indexed types.

Datakinds?

https://stackoverflow.com/questions/20558648/what-is-the-datakinds-extension-of-haskell
https://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html




[Reply][About]
[<<][haskell][>>][..]