Can an Elm program ever be untyped?

Learn
10

There is one way we can sort of hide types in Elm, and that is “Jeremys Interface” (oh no!, not again…). The single function version of which is:

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 ()

This lets us return a value that contains rep but without exposing rep in the return type.

I believe the correct term for create is a hylomorphism which is an unfold and fold fused together or generate and interpret in one go.

type Counter
    = Counter CounterIF

type alias CounterIF =
    { value : Int
    , inc : () -> Counter
    }

type Rep
    = Rep Int

new : Int -> Counter
new n =
    let
        make : Rep -> Counter
        make rep =
            Counter
                { value =
                    case rep of
                        Rep x ->
                            x
                , inc =
                    \() ->
                        case rep of
                            Rep x ->
                                make (Rep (x + 1))
                }
    in
    make (Rep n)

Rep never appears in the resulting API. Only Counter does. So the outside world can’t name Rep, construct it, or inspect it. From the outside we know it exists but that is all.

This is existential typing:

∃ t . Interface(t)

There exists some type t, but you are not allowed to know what it is.
You only get operations defined by the interface.

And not ad-hoc typing:

∀ t . If t has property P, then operations exist

Behaviour depends on which type t actually is.

Which is overloading / typeclass / polymorphic dispatch.

I was argued against so vehemently on Slack that Jeremys Interface is ad-hoc typing and not existential, that I gave in to believing that to be true. If it were true, then we really could create new typeclasses in Elm and get polymorphic dispatch. Turns out it isn’t true and I was right all along to identify it as existential typing. No loop holes here!