SMLFamily / Successor-ML

A version of the 1997 SML definition with corrections and some proposed Successor ML features added.
193 stars 10 forks source link

Lack of expressivity of functors (type variables). #24

Open Ud71p opened 8 years ago

Ud71p commented 8 years ago

We present a method for reuse of implementation, where one datastructure can be defined in terms of another, similar one. We utilize SMLs module language to transform a given datastructure into a new one.

Let's look at the set/map duality. If we have a map (aka. finite map, dictionary, table, etc.) datastructure, then we can easily implement a set in terms of it:

{ a, b, c } = { a:(), b:(), c:() },

that is a set of elements of type E can be represented as a map from keys of type E to values of type unit (empty tuples).

Likewise, if we have a set datastructure, we can use it to implement a map:

{ a:x, b:y, c:z } = { (a,x), (b,y), (c,z) }, a < b iff (a,) < (b,)

that is a map from keys of type K to values of type V can be represented as a set of elements of type K*V, i.e. key-value pairs. The ordering supplied to the given set implementation shall compare the pairs by first constituent only.

Observing this duality prevents the common mistake of duplicate implementation. The functions operating on sets and maps are practically the same, they may be long, and there is many of them in a rich set/map structure. Hence, one shall only implement a set directly, and then use it to implement a map. Alternatively, one can start by implementing a map, and implement a set in terms of it. In StandardML one should be able to use a functor to easily implement one datastructure in terms of another.

The preferred way would be to implement the set directly, and use a functor to transform it to a map. Why set? Because it's slightly easier and more elegant to implement - the internal datastructure only needs to store one value - the element, instead of two - keys and values.

However (due to a problem described later), we implement a map directly and later transform it into a set.

The signatures used here are pretty much the same as ORD_KEY, ORD_SET and ORD_MAP in SML/NJ. *)

(* Signature for our ordered type: *)

signature Comparable = sig type T val compare: T*T -> order end

signature MAP = sig type Key type 'v Map val empty: 'v Map val put: Key -> 'v -> 'v Map -> 'v Map end

(* The map datastructure is implemented directly: ) functor Map(comparable: Comparable) :> MAP where type Key = comparable.T = struct type Key = comparable.T datatype 'v Map = Empty | Binary of 'v Map * Key * 'v \ 'v Map val empty = Empty

(* This implementation lacks any form of balancing, so a better map would be even more complicated. *)

fun put k' v' Empty = Binary(Empty, k', v', Empty) | put k' v' (Binary(l,k,v,r)) = case comparable.compare(k',k) of LESS => Binary(put k' v' l, k, v, r) | EQUAL => Binary(l, k', v', r) | GREATER => Binary(l, k, v, put k' v' r) end

signature SET = sig type Element type Set val empty: Set val put: Element -> Set -> Set end

(* The set datastructure uses map internally, so the many long ) ( functions (like put) don't need to be repeated: *) functor Set(comparable: Comparable) :> SET where type Element = comparable.T = struct type Element = comparable.T structure M :> MAP where type Key = Element = Map(comparable) type Set = unit M.Map

val empty = M.empty fun put x s = M.put x () s end

(* Some usage examples: *) structure ComparableInt = struct type T = int val compare = Int.compare end

structure IMap :> MAP where type Key = int = Map(ComparableInt) structure ISet :> SET where type Element = int = Set(ComparableInt)

val set : ISet.Set = ISet.put 8 ISet.empty

(* Good, maps are polymorphic over values: *) val i2s : string IMap.Map = IMap.put 8 "a" IMap.empty val i2c : char IMap.Map = IMap.put 8 #"a" IMap.empty

(*

To summarize, we implemeted the map directly, and then used it to implement the set.

Now assume we want to go the other way around - first implement the set directly. We encounter a problem when trying to use it to define a map. It was easy taking a polymorphic type 'v Map, instantiate 'v to unit and get monomorhic type of sets. But the reverse seems impossible. How can one take a monomorhic set type and use it as a polymorphic 'v Map? Note that the map functor shall not bind the value type. The value type shall stay polymorphic, and only the key type shall be bound in the resulting structure. So the map functor can only take the key type as argument. In other words, we don't want IntToStringMap.Map, but we want (string IntMap.map).

It's quite natural that one should be able to go both ways. Therefore, I consider this as a shortcoming of StandardML - an example of a slight lack of expressivity of the module language.

How could this be fixed in SuccessorML?

*)

rossberg commented 8 years ago

For that you'd need applicative functors.

eduardoleon commented 8 years ago

I don't think it's more elegant to recover maps from sets. It's simpler and better to do it the other way around: a set is a map whose associated element type is unit. Including an associated element by default, and setting it to unit whenever it's not needed, has other benefits too: it aids data structural bootstrapping, a general technique for building efficient and complete data structures from inefficient and/or incomplete ones.

YawarRaza7349 commented 9 months ago

Trying to figure out why this can't work broke my brain, but I think I figured out one problem at least: Going from Set to 'v Map would result in the Set -> Set from put turning into something more like (forall 'v. 'v Map) -> (forall 'v. 'v Map) (equivalent to forall 'v1. (forall 'v2. 'v2 Map) -> 'v1 Map) rather than the desired forall 'v. 'v Map -> 'v Map. There isn't really a way to turn a particular function of the former into one of the latter.

The problem is that by the time you have a structure of signature SET, its Element type is monomorphized, and it "forgot" that it was created in a polymorphic way, so it can't be generalized back.

A related problem is that SML doesn't have a way to turn the monomorphic type Element into a polymorphic type 'v Element = M.Key * 'v. What's interesting is that, in isolation, this issue could be "fixed" by imagining all types as having an infinite number of phantom type variables, but then you still run into issues like the first thing I mentioned, not to mention the mind**** of thinking about how the prenex restriction behaves a language where every named type has the form forall (* infinite type variables *). (* ... *).

rossberg commented 9 months ago

All type-theoretic considerations aside, the idea of abstracting a type declaration after the fact by somehow injecting type parameters reminds me suspiciously of aspect-oriented programming, which essentially is an attempt to allow something analogous on the term level. And we all remember how great an idea that was.