Demystifying Jeremy's Interfaces

Variant #1: Type Parameters and New Initialization

See posts Remove the Record Constructor Function and Redesigned Initialization


Types

type Counter
    = Counter (CounterOperations Counter)


type alias CounterOperations t =
    { up : Int -> t
    , down : Int -> t
    , value : Int
    , reset : () -> t
    }
  • operations type with type parameter
  • explicit thunk in reset operation

Utility Functions

up : Int -> Counter -> Counter
up n (Counter counterOperations) =
    counterOperations.up n


down : Int -> Counter -> Counter
down n (Counter counterOperations) =
    counterOperations.down n


value : Counter -> Int
value (Counter counterOperations) =
    counterOperations.value


reset : Counter -> Counter
reset (Counter counterOperations) =
    counterOperations.reset ()
  • additional () parameter in reset function

Implementation

counterImplInt : (Int -> Counter) -> Int -> CounterOperations Counter
counterImplInt raise rep =
    { up = \n -> rep + n |> raise
    , down = \n -> rep - n |> raise
    , value = rep
    , reset = \() -> 0 |> raise
    }


counterImplList : (List () -> Counter) -> List () -> CounterOperations Counter
counterImplList raise rep =
    { up = \n -> List.repeat n () ++ rep |> raise
    , down = \n -> List.drop n rep |> raise
    , value = List.length rep
    , reset = \() -> [] |> raise
    }
  • records instead of record creator function
  • every implementation has to apply the raise function
  • every implementation has to account for laziness in the reset function

Instance Creation

intCounter : Int -> Counter
intCounter start =
    IF.create Counter counterImplInt start


listCounter : Int -> Counter
listCounter start =
    IF.create Counter counterImplList (List.repeat start ())
  • no restriction on how to create the initial internal value

Interface Module

create : (ops -> typ) -> ((rep -> typ) -> rep -> ops) -> rep -> typ
create constructor impl =
    let
        repTyp : rep -> typ
        repTyp rep =
            constructor (impl repTyp rep)
    in
    repTyp
  • :sparkles: magic :sparkles: condensed in a single function

Variant #2: Separated Definitions and Implementations

See post Separate Interface from Implementation


Types

type Counter
    = Counter (CounterOperations Counter)


type alias CounterOperations t =
    { up : Int -> t
    , down : Int -> t
    , value : Int
    , reset : () -> t
    }
  • operations type with type parameter
  • explicit thunk in reset operation

Utility Functions

up : Int -> Counter -> Counter
up n (Counter counterOperations) =
    counterOperations.up n


down : Int -> Counter -> Counter
down n (Counter counterOperations) =
    counterOperations.down n


value : Counter -> Int
value (Counter counterOperations) =
    counterOperations.value


reset : Counter -> Counter
reset (Counter counterOperations) =
    counterOperations.reset ()
  • additional () parameter in reset function

Mapping of Operations

counterOps : (rep -> typ) -> CounterOperations rep -> CounterOperations typ
counterOps raise ops =
    { up = ops.up >> raise
    , down = ops.down >> raise
    , value = ops.value
    , reset = ops.reset >> raise
    }
  • applying the raise function centralized in map-like function

Implementation

counterImplInt : Int -> CounterOperations Int
counterImplInt rep =
    { up = \n -> rep + n
    , down = \n -> rep - n
    , value = rep
    , reset = \() -> 0
    }


counterImplList : List () -> CounterOperations (List ())
counterImplList rep =
    { up = \n -> List.repeat n () ++ rep
    , down = \n -> List.drop n rep
    , value = List.length rep
    , reset = \() -> []
    }
  • records instead of record creator function
  • implementations only have to deal with their internal type rep
  • every implementation has to account for laziness in the reset function

Instance Creation

intCounter : Int -> Counter
intCounter start =
    IF.create Counter counterOps counterImplInt start


listCounter : Int -> Counter
listCounter start =
    IF.create Counter counterOps counterImplList (List.repeat start ())
  • no restriction on how to create the initial internal value

Interface Module

create : (opsTyp -> typ) -> ((rep -> typ) -> opsRep -> opsTyp) -> (rep -> opsRep) -> (rep -> typ)
create constructor mapOps impl =
    let
        raise : rep -> typ
        raise rep =
            constructor (mapOps raise (impl rep))
    in
    raise
  • :sparkles: magic :sparkles: condensed in a single function

Variant #3: Implicit Laziness

See post Add Laziness


Types

type Counter
    = Counter (CounterOperations (() -> Counter))


type alias CounterOperations t =
    { up : Int -> t
    , down : Int -> t
    , value : Int
    , reset : t
    }
  • operations type with type parameter
  • single explicit thunk in interface type

Utility Functions

up : Int -> Counter -> Counter
up n (Counter counterOperations) =
    counterOperations.up n ()


down : Int -> Counter -> Counter
down n (Counter counterOperations) =
    counterOperations.down n ()


value : Counter -> Int
value (Counter counterOperations) =
    counterOperations.value


reset : Counter -> Counter
reset (Counter counterOperations) =
    counterOperations.reset ()
  • additional () parameter in several functions

Mapping of Operations

counterOps : (rep -> typ) -> CounterOperations rep -> CounterOperations typ
counterOps raise ops =
    { up = ops.up >> raise
    , down = ops.down >> raise
    , value = ops.value
    , reset = ops.reset |> raise
    }
  • applying the raise function centralized in map-like function

Implementation

counterImplInt : Int -> CounterOperations Int
counterImplInt rep =
    { up = \n -> rep + n
    , down = \n -> rep - n
    , value = rep
    , reset = 0
    }


counterImplList : List () -> CounterOperations (List ())
counterImplList rep =
    { up = \n -> List.repeat n () ++ rep
    , down = \n -> List.drop n rep
    , value = List.length rep
    , reset = []
    }
  • records instead of record creator function
  • implementations only have to deal with their internal type rep
  • implementation don’t have to account for laziness

Instance Creation

intCounter : Int -> Counter
intCounter start =
    IF.create Counter counterOps counterImplInt start


listCounter : Int -> Counter
listCounter start =
    IF.create Counter counterOps counterImplList (List.repeat start ())
  • no restriction on how to create the initial internal value

Interface Module

create : (opsTyp -> typ) -> ((rep -> () -> typ) -> opsRep -> opsTyp) -> (rep -> opsRep) -> (rep -> typ)
create constructor mapOps impl rep =
    let
        raise : rep -> () -> typ
        raise rep_ () =
            constructor (mapOps raise (impl rep_))
    in
    raise rep ()
  • laziness is handled here and in the utility functions
  • :sparkles: magic :sparkles: condensed in a single function

 


I really, really thought that this would be the last part of the series. But then came @hayleigh on the Elm slack.

Hold on for one last thing…

2 Likes

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 :heart_eyes:


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!

8 Likes

Well, what can I say except:

Oh, this looks nice :heart_eyes:
Very abstract and general. I like it.

I wonder why does haskell write an existential as forall x? and not exists x? Is it because the x always appears in the argument position to the CE constructor, and therefore flips the universal quantifier to an existential one? (Come on brain, its not like a I didn’t do this for my undergrad dissertation 25 years ago…)

1 Like

The whole thing is so well written, made me smile a lot. Nice ending. Nice to have this in the toolbox.
So far i’ve only needed similar patterns, like

  • functionalization of only the shared “observe” functions (example)
  • storing a toBroad function alongside so that builders can always transform it to a common base type without needing to |> build/finish the specialized part builder
    type Expression = IntExpression IntExpression | ...
    type alias IntExpression = { value : Int, base : Base16 | Base10 }
    
    type alias ExpressionBuilder specific =
        { specific : specific, toExpression : specific -> Expression }
    declarationFunction : { expression : ExpressionBuilder specific, ... } -> ...
    expressionInt : Int -> ExpressionBuilder IntExpression
    

Btw the last one I don’t like in practice because the builders don’t compose/mix easily and in other situations it might not be so clear what the toBroad function should convert to. Use with caution.

Being able to modify a functionalized thing seems powerful! Thanks for this series

2 Likes

Thank you for demystifying all of this in a brilliant way. You saved me a lot of work (as for many people I’m pretty sure). Now that we have both interface and sum types, the next thing that could be interesting would be to identify precisely in which case we prefer sum types over interfaces (and vice-versa) and identify their meaning (in an abstract way).
The first thing that come to my mind where I would prefer a sum type is error handling. Is there something else? Can we define a semantic for each way of doing? Thanks to you I can ask myself those “abstract” questions with good tools in my hand !

1 Like

Thank you all for the kind words. They mean a lot to me.

More Studies on Interfaces

My initial motivation was just to understand how Jeremy’s magic code works. Then I wanted to share what I had learned. The result grew much bigger than expected, both in space and time. Having neither a concrete use case nor the theoretical background to explore this further, I’ll leave it as it is.

Sum Types

Arthur mentioned sum types in his reply. Hayleigh’s paper shows yet another way to implement lists of heterogeneous values: “Bringing different types into union”.

The basis is this sum type:

type Sum l r
    = InL l
    | InR r

This technique isn’t quite as easy to use as interfaces, but it allows to combine heterogeneous values without having to hide the underlying types.

On the plus side, this allows to get back at the original value. For the counter example, we could get the current Int or the current List (), because we know the types at all positions in the list.

On the minus side, this can yield very long types. Here’s the type for a list of just four counters with the underlying types Int, List (), Int, and again List ():

CounterList (Sum Int (Sum (List ()) (Sum Int (Sum (List ()) Nil))))

I implemented a list of heterogeneous counters using this technique to get a feel for it. If you are interested, I can publish the code, but I would start a new topic for that.

Easter Egg

I’m surprised that so far no one has asked about the animated

in the table of contents at the end of my last post. It was supposed to be a hint for an SVG animation that I have prepared, but maybe the hint was too subtle :slightly_smiling_face: The animation isn’t very spectacular, just some moving texts.

I originally planned for the animation to start when the reader clicks on the wiggling :interrobang:. 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.

Edit: Done

2 Likes

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.