One Last Thing
Is this the real life? Is this just fantasy?
Once again, Jeremy is visiting the type systems demons and wizards conference. But after he returns this time, he seems to be somehow changed. Rupert talks to him about it.
Rupert
Jeremy, how was the conference? You seem to be somewhat… lost in thought since then.
Jeremy
The conference was great as always, thank you Rupert. You’re right, though. There’s something that keeps bothering me.
At the conference, Hayleigh, a type system demoness I already met several times before, gave a great talk about eliminating recursive existential data types.
Rupert
About what?
Jeremy
Oh, the topic isn’t relevant here. But in her talk, Hayleigh mentioned the following web page: Representing existential data types with isomorphic simple types. When I briefly skimmed the contents to get to the chapter about recursive existentials, I stumbled upon the following sentence:
“We thus observe the other, related benefit of existentials: supporting implicitly heterogeneous lists – lists of elements of different types but with a common set of operations.”
Rupert
Isn’t this what we’re doing with interfaces: supporting lists of different implementations of an interface, where the interface type defines the common set of operations?
Jeremy
Yes, exactly.
Rupert
Interesting. So are “existentials” the same as interfaces? Is there any code in the article?
Jeremy
Yes, there is code, but it’s Haskell code, as usual. If you’re interested, I can briefly describe the idea, and if you have some time, I can also show you how to translate all this into Elm.
Rupert
Of course I’m interested, and I’ll take as much time as necessary.
Jeremy
OK. In the article they talk about “packages”. You can think of such a “package” as an Elm module which exposes an opaque type. Let’s call the type x.
Now you, as the user of the module, what can you do with a value of this type x?
Rupert
Hmm. As I don’t know anything about the opaque type x, I think I can’t do anything with such a value?
Jeremy
Right. Yet many, or maybe even most Elm packages contain modules exposing at least one opaque type. For example, the Set type in the Set module of the “elm/core” package is an opaque type. I’m sure you have used Sets before?
Rupert
Yes.
Ah, I see what you’re getting at: the Set module defines functions for creating and using values of type Set.
Jeremy
Correct. The article talks about three different, general types of functions which could be provided by such a “package”:
| name |
type |
purpose |
| init |
i -> x |
creating a value of the opaque type x from a value of some type i |
| modify |
x -> m -> x |
modifying a value of type x using a value of some type m |
| observe |
x -> o |
getting some information of type o from a value of type x |
Rupert
Very abstract and general. I like it.
Jeremy
OK. Now to existentials…
In Haskell, we could describe such a general “package” with the following type:
data CE i m o =
forall x. CE x (i -> x) (x -> m -> x) (x -> o)
You see that in the CE constructor there’s a value of type x, as well as the 3 general functions from above.
The forall x. part is the existential. It basically means that in every CE there exists a type x, but it could be any type. Because of the existential, the type CE has only the type parameters i, m, and o, but not x. The type x is hidden inside.
In Elm, we don’t have existentials. Here, the type CE could be defined as
type CE i m o x
= CE x (i -> x) (x -> m -> x) (x -> o)
Because of the missing existential, we have to make the type x explicit as a type parameter of the type CE.
Rupert
I think I understand this. It means that, in Haskell, we could create a list of CE i m o values with different x types, but in Elm we can’t.
Jeremy
Right.
Rupert
But we can use interfaces in Elm.
Jeremy
Yes, we can, but there’s another way. In the article they show a different, yet similar technique:
In Haskell, the type CE i m o is equivalent (“isomorph”) to the following type:
data C1 m o =
C1 (m -> C1 m o) o
In Elm this definition is identical:
type C1 m o
= C1 (m -> C1 m o) o
Rupert
But how can this be equivalent? Where’s the type parameter i, and in Elm, where’s the x?
Jeremy
If two types are “equivalent”, or “isomorph”, it means that, given a value of one type, we can transform it into a value of the other type and vice versa.
And indeed, in the article they show the code for the two transformation functions. We can even implement them in Elm!
Rupert
Please go on. I want to see them.
Jeremy
Ok, first the function from CE to C1:
isoCEC1 : CE i m o x -> ( C1 m o, i -> C1 m o )
isoCEC1 (CE x init modify observe) =
let
makeC1 : x -> C1 m o
makeC1 x_ =
C1 (makeC1 << modify x_) (observe x_)
in
( makeC1 x, \i -> makeC1 (init i) )
As you can see, the function creates a value of type C1 m o plus an initialization function i -> C1 m o.
Rupert
OK. The constructor function is where the i type parameter went to.
The let with the recursive makeC1 function reminds me of our interface module’s create function.
Jeremy
Yes. The types are very different though. I’ll come back to this.
Now the reverse function from C1 to CE. Again, we start with both a value of type C1 m o plus an initialization function i -> C1 m o:
isoC1CE : ( C1 m o, i -> C1 m o ) -> CE i m o (C1 m o)
isoC1CE ( c1, initC1 ) =
let
init : i -> C1 m o
init =
initC1
modify : C1 m o -> m -> C1 m o
modify (C1 modifyC1 _) =
modifyC1
observe : C1 m o -> o
observe (C1 _ observeC1) =
observeC1
in
CE c1 init modify observe
Rupert
Jeremy, you’re cheating! You don’t return a type x, but instead use the thing we already have, a C1 m o!
Jeremy
No, this is not cheating.
Remember the Haskell type CE i m o where the x could be hidden, because it can be anything? In Elm we have to explicitly specify the type parameter, but it still can be anything! And in this case we simply chose the type C1 m o for the x.
In order to create a value of type CE i m o (in Elm CE i m o x), you just have to prove that there exists a type x by providing a value of this type plus the accompanying functions, but it doesn’t matter which type you choose. That’s why it’s called “existentials”.
Rupert
I trust you, but I have to think about this some more…
Jeremy
Yeah. This is confusing at first.
Back to the resemblance to interfaces. I’m sure you remember how we removed the initialization of the internal representation (the i -> x function) from the interface code? And that our “IF.create” functions just return a constructor function of type x -> C1 (where C1 is the interface type)?
If we do the same with the isoCEC1 function and remove the type CE, we get this:
type C1 m o
= C1 (m -> C1 m o) o
createC1 : (x -> m -> x) -> (x -> o) -> (x -> C1 m o)
createC1 modify observe =
let
makeC1 : x -> C1 m o
makeC1 x =
C1 (makeC1 << modify x) (observe x)
in
makeC1
Rupert
Oh, this looks nice 
Jeremy
Yes it does! Here are some differences, I’d even say: improvements, to the “IF.create” interface functions:
-
We don’t need to define a record type with the interface operations.
-
Without a single operations record type, we are free to choose different shapes for the operations provided by the “interface implementer” (the input to the createC1 function) and the operations used by the “interface definer” (the definition of type C1). In both places, we can independently choose any product type, for example custom types like CE and C1 above, records as in the interface examples, tuples, and so on.
-
The functions provided by the “interface implementer” can have more familiar signatures like x -> m -> x or x -> o, instead of, for example, x -> { modify : m -> x, observe : o }.
Rupert
Do you think that, for comparison, we can implement the Counter interface using this new technique?
Jeremy
Of course we can. I did this already. Here’s the part of the “interface definer”:
type Counter
= Counter (Int -> Counter) (Int -> Counter) Int (() -> Counter)
up : Int -> Counter -> Counter
up n (Counter upCounter _ _ _) =
upCounter n
down : Int -> Counter -> Counter
down n (Counter _ downCounter _ _) =
downCounter n
value : Counter -> Int
value (Counter _ _ valueCounter _) =
valueCounter
reset : Counter -> Counter
reset (Counter _ _ _ resetCounter) =
resetCounter ()
create : (x -> Int -> x) -> (x -> Int -> x) -> (x -> Int) -> x -> (x -> Counter)
create upX downX valueX resetX =
let
raise : x -> Counter
raise x =
Counter
(\n -> upX x n |> raise)
(\n -> downX x n |> raise)
(valueX x)
(\() -> resetX |> raise)
in
raise
You can see that I didn’t choose records in this example, too, but we are free to use records for, say, better readability.
Rupert
Wow. This really looks nice and clean! And I see that you also explicitly added laziness to the reset operation!
Jeremy
Yes. It’s not more work than in the interface versions! And it is hidden from the “interface implementer”, whose code is here:
fromInt : Int -> Counter
fromInt =
create (+) (-) identity 0
fromList : List () -> Counter
fromList =
create
(\l n -> List.repeat n () ++ l)
(\l n -> List.drop n l)
List.length
[]
Rupert
Again: wow! This is… simply fantastic! No raising and no laziness needed here!
Jeremy
I like this very much, too. To create an instance, we just have to build the initial internal value, as before:
intCounter : Int -> Counter
intCounter start =
fromInt start
listCounter : Int -> Counter
listCounter start =
fromList (List.repeat start ())
And you know what, Rupert? Even if we use records as in the interface versions, this code is even faster than the fastest interface variant, according to my simple benchmarks.
Rupert
But all this is just great! What bothers you?
Jeremy
Yeah, I’m fascinated too. And I’m not really bothered. It’s just that… using this implementation, we don’t need the interface module anymore, and this makes me think about “the life of a module”:
In the beginning, it was a module with five functions and some inherent magic. Then we reduced it to just one magic “create” function in various variants, and now it all just… vanishes into thin air?
Rupert
I see. Everything is dust in the wind.
-- THE END --
I mentioned before that I love stories with happy ends, and I dislike open ends just as much. But it is as it is…
So what will remain of all this?
I don’t know…
A BIG thank you goes to Rupert, Mark, Abastro, and Arthur for their comments, and of course to Jeremy and Hayleigh for bringing all this to my attention.
Thank you!
magic 
The animation isn’t very spectacular, just some moving texts.
. Unfortunately I haven’t found a way to react to mouse clicks in this Discourse. Therefore I’ll perform the mouse click “manually” by editing the post, let’s say in about 24 hours, and then the animation will start automatically.