2 ms·

None of Idris, Ceylon or F# doesn't have ML-style modules: (0) “In principle”, you could encode modules in Idris using dependent sum types, but... Good luck wi

None of Idris, Ceylon or F# doesn't have ML-style modules: (0) “In principle”, you could encode modules in Idris using dependent sum types, but... Good luck with that! It isn't going to be terribly usable. In general, Haskell and related languages don't consider it worth the effort to give modules proper types. I guess we can be thankful Agda's modules don't suck as badly as Haskell's - at least they can be nested. (1) Ceylon and Scala's type systems are sophisticated enough to encode some of the use cases for modules with objects, but invariably the result is awkward. And other use cases are just impossible. For example, how should I encode an ML functor that takes as arguments two modules with shared type members? If it's possible at all, I don't even want to imagine how horrifying it will be to manually turn all the sharing by fibration into sharing by parameterization. (2) F# doesn't allow any encoding of ML-style modules. Nothing. Nichts. Nada. It's the only so-called “ML dialect” where the most important feature from ML is completely missing.

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 ago
  ML'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.

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 ago
ML'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.