Can an Elm program ever be untyped?

[rupert]

Elm has polymorphism, but we usually cannot create polymorphic values. An example:

foldr : (a -> b -> b) -> b -> List a -> b

To call this, I need a list of something:

foldr (\w acc -> w ++ " " ++ acc) "" ["words", "to", "join", "with", "spaces"]

Its polymorphic, but I needed to give it some values to do anything useful, and that means that the program ended up fully typed at runtime. Ok, I don’t have to give it concrete values immediately, the polymorphism could continue up the call stack as many times as we like, but ultimately somewhere has to provide real values.

Also worth noting that the empty list can be polymorphic (List a); in some sense all empty lists are equivalent despite their possible differences in type.

---

There is a way in Elm that I can create a non-empty value that has a variable type:

num : number
num = 1

Elm does not require that Float has a decimal point in it, so when I write an integer it can be Int or Float until the type checker constrains it one way or the other.

But will that always happen ?

---

Elm Programs can have arbitrary type variables. You might know this from having done some fancy thing with Programs in the past. It is possible for unconstrained type variables to bubble all the way up to the Program level, and they can then escape the Program entirely there:

main : Program () (Model number) Msg

So now I can have:

type alias Model number =
    { count : number }

And I can really instantiate that with a variably typed value, see num above.

But can I ever instantiate it with a value that is not actually an Int?

untypedModel : Bool -> Model number
untypedModel isInt =
    if isInt then
        { count = 1 }
    else 
        { count = 1.0 }

But that won’t pass typechecking, since both branches must have the same type, they unify to Model Float and that is not the same as Model number:

Something is off with the 2nd branch of this `if` expression:

23|         { count = 1.0 }
            ^^^^^^^^^^^^^^^
The 2nd branch is a record of type:

    { count : Float }

But the type annotation on `untypedModel` says it should be:

    Model number

I also tried passing in a number as a flag:

main : Program number (Model number) Msg

And the type checker also rejected that:

Your `main` program wants an unspecified type from JavaScript.

55| main =
    ^^^^
But type variables like `number` cannot be given as flags. I need to know
exactly what type of data I am getting, so I can guarantee that unexpected data
cannot sneak in and crash the Elm program.

---

If we took an Elm program and type checked it, then replaced all occurences of values with number type that remain with Int, I think the result would be an Elm program that still type checked and had the exact same runtime behaviour as the original.

I don’t believe there are any other ways in Elm that we can create instances of values that are untyped.

Therefore, even though Elm programs can be polymorphic, they can never be untyped.

I just wanted to check that my reasoning here is sound, and that there is nothing I have missed ? no sneaky workarounds ? No devious type shenanigans that would falsify that assertion ?

[rupert]

Ellie in case you wanted to fiddle around with it: https://ellie-app.com/xVfKVgBKs3Xa1

[wolfadex]

Does this count since we never define msg?

main : Html msg
main =
  Html.text "Hello"

[rupert]

No, since msg here is effectively empty - I count it in the same category as List a, polymorphic but you never actually create an untyped value of anything.

[allanderek]

Doing something like:

let
   l : number
   l = [ 1, 2, 3 ]
in
List.any (\x -> x > 2) l

Is not what you’re looking for right? In this case l really is of type List number and we consume it without ever resolving its type. I’ve even done a bit more with l than was strictly needed, I could have done something like List.length l, but that would feel like I was deliberately ‘throwing away the values’. In the example above I don’t throw away the values. Though, the example above is a bit contrived in that I could have written l : Int to no ill effect.

[rupert]

@allanderek

let
   l : List number -- List number!
   l = [ 1, 2, 3 ]
in
List.any (\x -> x > 2) l

Good example, thanks. The result of this is Bool. So what is interesting about this example is that it uses number in a computation, but the result type is Bool. So the use of values that are not strictly typed is only temporary, and does not escape this context into the wider program.

But as you say, change number to Int and it works just the same. I think changing values from number to Int should always be safe, after type checking. After type checking so that number is not unified to Float.

To be more precise about what an ‘untyped program’ would be: One that can run with values that can have more than one type, but are somehow coerced into being untyped (represented as a type variable or their types made to dissapear somehow), yet the program still runs. So this program is almost that, but in reality the only type it can actually run over is Int.

[allanderek]

So the use of values that are not strictly typed is only temporary, and does not escape this context into the wider program.

Although I could have done List.maximum l, which would have resulted in a Maybe number.

Ultimately you’re going to do something with the number, since we don’t have a generic String.fromX or even String.fromNumber.

So this program is almost that, but in reality the only type it can actually run over is Int.

Except that l : List Float would also work.

But I get that this example is not quite hitting the potential problem you are thinking of.

[rupert]

@allanderek

So this program is almost that, but in reality the only type it can actually run over is Int.

Except that l : List Float would also work.

So this program is almost that, but in reality the only type it can actually run over is Int or Float, but only one of those in any given version of the program!

I think it is an imaginary problem, and Elms type system is completely sound.

[allanderek]

I think the way to summarise this is: If a value is of type number then it really is safe to use it as either an Int or a Float. Similarly “empty” values, such as List a really are safe to use as though they are any kind of list (because they don’t have any a values in them).

[rupert]

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.

Existential Types in Elm

BTW - I was wrong to call them existential types. I think it is more accurate to describe this as ad-hoc polymorphism.

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!