4 ms·
One of the classic motivating examples (which is addressed in the 1ML paper) goes like this: Both trees and hash tables can be used to implement map-like data
by andolanra 11y ago
One of the classic motivating examples (which is addressed in the 1ML paper) goes like this:
Both trees and hash tables can be used to implement map-like data structures. You could, in ML, have an abstract signature for Map types that gets implemented sometimes by a concrete TreeMap implementation and sometimes by a concrete HashMap implementation. HashMap would be a better choice if the expected number of entries is larger, and the TreeMap would be better if the expected number of entries is smaller, so what we'd like to do is write something like
module Map = if size > threshold then HashMap else TreeMap
so that we choose what concrete implementation we want at runtime—but we can't really do that, because the language we use to talk about modules in ML is distinct from the language we use to talk about values. That is to say, the size > threshold part can't coexist in the same expression with the HashMap and TreeMap part. Some MLs have added the ability to wrap modules in values, so you can write it this in OCaml:
module Map = (val (if size > threshold
then (module HashMap : MAP)
else (module TreeMap : MAP))) : MAP
but it's a bit awkward because of the explicit moving-back-and-forth between value-level and module-level, and the interaction between the two languages has some rough edges (which the paper explains more thoroughly, if you're interested.)
The motivation for 1ML is that we'd like to use the same language to talk about both modules and values. That way, we could write the first, simpler definition without having to worry about the fact that we're manipulating distinct 'things'. Of course, there are other tradeoffs involved in the 1ML solution, but it's an interesting, compelling experiment.
- hoprocker 11y agoThanks for pulling this out and explaining it; although I'm not familiar with ML, I get what the problem is here. Interesting!
- rtpg 11y agohow does that end up working for typechecking? does the Map module end up having all the properties of the intersection of these elements? The Map example seems pretty easily solvable via Haskell through typeclasses or the more standard OOP-y languages through interfaces, but am I missing something? Does SML not have the tools for this right now?
- andolanra 11y agoThere are very much ways of expressing that computation in SML—or in Haskell or other languages—but not in the language of modules. Haskell typeclasses would have a similar problem. Consider the following pseudocode: class Map m where {- some implementation -} instance Map HashMap where {- ... -} instance Map TreeMap where {- ... -} mkMap :: Int -> {- ??? -} mkMap size | size > threshold = newHashMap | otherwise = newTreeMap What is the type of mkMap? It won't actually type-check in Haskell. It can't be (Map m) => m, because it needs to have a concrete type. We could do some kind of type-level work, relect the size variable into the type level, and have a type family that decides whether the resulting type is a HashMap or a TreeMap—but that has the same problem as the OCaml example, where we're using a different language (the language of type-level computation) to talk about something that'd be simple with value-level programming. One place where you could write this easily is in a dynamically typed language: def mkMap(size): if size > threshold: return HashMap() else: return TreeMap() That is exactly why this kind of research is interesting: we'd like to capture the flexibility of idioms that dynamic languages can sometimes afford us, with the extra safety and security guarantees of a static type system!
- mercurial 11y agoYou don't need a dynamic language for that. In Java: Map<K,V> mkMap(int size) { return size > threshold ? new HashMap<K,V>() : new TreeMap<K,V>(); }
- octatoan 11y agoIf I remember correctly, isn't this one of the problems Idris and Agda are good at solving?
- andolanra 11y agoWe could in fact write mkMap in Idris with very little change, and give it a proper type: -- This might not be the best/cleanest way of writing it, as my -- Idris is a little rusty, but this will work: mkMap : (size: Int) -> (if size > threshold then HashMap else TreeMap) mkMap size with (size > threshold) | True = newHashMap | False = newTreeMap So yes, although again, other tradeoffs are made to allow this kind of radical expressiveness.