3 ms·
You could encode a module as a record with a stored type and functions for it for Idris. Then you can simply create functors as functions that take one type of
by nv-vn 11y ago
You could encode a module as a record with a stored type and functions for it for Idris. Then you can simply create functors as functions that take one type of record in and return another type. The syntax is ugly, but you can define macros to make it slightly more appealing. It's not an optimal approach because of namespacing of record fields, but I remember hearing that one of the next few Idris releases was going to change how record fields get namespaces.
- catnaroek 11y agoML's module language has subtyping. Given any module signature, you can obtain a supersignature by forgetting any of the following: (0) The presence of a value component. (1) The presence of a type component. (2) The concrete definition of a type component, while still remembering its presence. I am not sure you can do this in Idris, other than manually shuffling data between multiple dependent record types. Which is rather inconvenient: If you have a module with 20 components, the last thing you want to do is manually shift 15 of them to another module. Also, unlike vanilla Haskell (no extensions) type classes, which can only have a single type parameter, ML modules can have more than one type component.