Inconsistency/unsoundness in type system due to channels

[imeckler]

Probably this is well known, but I couldn't find an issue on here. Because there's no value restriction on channels in Elm, the type system is unsound (for an appropriate notion of unsoundness) in the usual way. The following incorrect program compiles.

import Signal
import Html
import Html.Attributes(style)
import Html.Events(..)
import Maybe

c = Signal.channel Nothing

s : Signal Int
s = Signal.map (Maybe.withDefault 0) (Signal.subscribe c)

draw x =
  Html.div
  [ onClick (Signal.send c (Just "I am not an Int"))
  , style [("width", "100px"), ("height", "100px")]
  ]
  [ Html.text (toString (x + 1)) ]
  |> Html.toElement 100 100

main = Signal.map draw s

[johnpmayer]

Whoa nice catch. Bug with type unification
On Feb 5, 2015 9:50 AM, "imeckler" notifications@github.com wrote:

Probably this is well known, but I couldn't find an issue on here. Because
there's no value restriction on channels in Elm, the type system is unsound
(for an appropriate notion of unsoundness) in the usual way. The following
incorrect program compiles.

import Signalimport Htmlimport Html.Attributes(style)import Html.Events(..)import Maybe
c = Signal.channel Nothing
s : Signal Ints = Signal.map (Maybe.withDefault 0) (Signal.subscribe c)
draw x =
Html.div
[ onClick (Signal.send c (Just "I am not an Int"))
, style [("width", "100px"), ("height", "100px")]
]
[ Html.text (toString (x + 1)) ]
|> Html.toElement 100 100
main = Signal.map draw s

—
Reply to this email directly or view it on GitHub
#889.

[johnpmayer]

Actually calling this a unification bug isn't quite right. It's because the
type of c is "Channel (Maybe a)" which unifies with both. So it's both
polymorphic and has a side effect of creating a channel. Maybe top level
definition for channels isn't a good idea - requiring them to be defined
with input ports (promises proposal) might just fix this.
On Feb 5, 2015 7:47 PM, "John Mayer" john.p.mayer.jr@gmail.com wrote:

Whoa nice catch. Bug with type unification
On Feb 5, 2015 9:50 AM, "imeckler" notifications@github.com wrote:

Probably this is well known, but I couldn't find an issue on here.
Because there's no value restriction on channels in Elm, the type system is
unsound (for an appropriate notion of unsoundness) in the usual way. The
following incorrect program compiles.

import Signalimport Htmlimport Html.Attributes(style)import Html.Events(..)import Maybe
c = Signal.channel Nothing
s : Signal Ints = Signal.map (Maybe.withDefault 0) (Signal.subscribe c)
draw x =
Html.div
[ onClick (Signal.send c (Just "I am not an Int"))
, style [("width", "100px"), ("height", "100px")]
]
[ Html.text (toString (x + 1)) ]
|> Html.toElement 100 100
main = Signal.map draw s

—
Reply to this email directly or view it on GitHub
#889.

[imeckler]

This is actually a well understood and solved problem. It's essentially the same issue as would arise with mutable references in SML or OCaml if not for the value restriction (a value restriction does bring issues of its own, but they're not that bad as they can generally be solved by eta expanding).

[evancz]

Is it possible to do this with any other functions in Elm? Am I correct that this is related to functions with effects, but otherwise it is not needed?

This is literally the only function in Elm that has side-effects, so if it is tied to effects, then I'd rather just get rid of channel. But does the same issue arise when you manage effects like in Haskell?

[imeckler]

I doubt it's possible to do this with anything else in Elm. This issue is generally tied to mutation. One might worry that one could try and pull the same trick with signals, but I guess it shouldn't be possible since there is some kind of pure model for the signature of Elm Signals provided by a stream type.

Things are quite a bit different in Haskell since the only place one "has" something of type (for example) IORef a for some a is in the second argument to bind and plain old unification can keep us from doing naughty things since we can never obtain something of type forall a. IORef (f a) (for some f) as we can in Elm. It's hard to imagine what the type of newIORef would even have to be to get it to return a polymorphic ref (the return value would have to be IO (forall a. IORef (...)), but there's nothing sensible to put in for ...).

Consider the following program (which is rejected by GHC) for example.

import Data.IORef
main = newIORef Nothing >>= \r -> writeIORef r (Just ()) >> writeIORef r (Just "no")

The lambda is typed as follows:

• r is given the type IORef (Maybe a) for a fresh type variable a. Note this is monomorphic!
• writeIORef r (Just ()) imposes the constraint a ~ ()
• writeIORef r (Just "no") imposes the constraint a ~ String, which can't be satisfied

If we use unsafePerfomIO, you can get a value of type forall a. IORef (Maybe a) and you get the same issue as in Elm.

Does the current promises proposal provide a way to write, e.g., the TodoMVC program without using channels?

[mgold]

The program still compiles when annotated with c : Signal.Channel (Maybe a). Why we accept monomorphic type variables in annotations is another discussion, but requiring a fully specified annotation would fix the issue. Ports require annotations, so that dovetails with the promises proposal, as John mentioned.

[polytypic]

I assume this is well known, but, for reference, here is the same unsoundness exposed using mailbox:

import Signal
import Html exposing (Html)
import Html.Attributes exposing (style)
import Html.Events exposing (..)
import Maybe

c = Signal.mailbox Nothing

s : Signal Int
s = Signal.map (Maybe.withDefault 0) c.signal

draw x =
  Html.div
  [ onClick c.address (Just "I am not an Int")
  , style [("width", "100px"), ("height", "100px")]
  ]
  [ Html.text (toString (x + 1)) ]
  |> Html.toElement 100 100

main = Signal.map draw s

[rtfeldman]

I don't think this is well known, but it's definitely a reproducible bug!

I pasted that code into the current (0.15.1) Try Elm; it compiled and ran, and when I clicked the "1", it turned into "I am not an Int1".

[rtfeldman]

To rule out a type inference bug, here is a minimal example with complete annotations that reproduces the bug in 0.15.1 if you paste it into Try Elm:

import Signal
import Html exposing (..)
import Html.Attributes exposing (..)
import Html.Events exposing (..)
import Maybe


maybeInts : Signal.Mailbox (Maybe a)
maybeInts =
    Signal.mailbox Nothing


ints : Signal Int
ints =
    Signal.map (Maybe.withDefault 0) maybeInts.signal


view : Int -> Html
view int =
    Html.div
        [onClick maybeInts.address (Just "I am not an Int")]
        [text (toString (int + 1))]


main : Signal Html
main =
    Signal.map view ints

If you try to change the type annotation on maybeInts from (Maybe a) to (Maybe Int) you do get a compile error.

[imeckler]

It's not a bug in the implementation. It's a bug in the type system resulting from the fact that Elm doesn't have a sort of value restriction, as mentioned above. One solution that I think Evan mentioned at some point would be to require mailboxes to have monomorphic types, which seems quite reasonable.

[mgold]

Yeah, a Signal a doesn't make a whole lot of sense. So this would be special casing mailboxes? I can see two cases. If there's no annotation, it should tell you to add one. If there is an annotation, it should tell you not to use type variables.

[jvoigtlaender]

A problem with the proposal to require mailboxes to have monomorphic types: What to do about cases like the implementation of start in start-app/StartApp.elm? See https://github.com/evancz/start-app/blob/2.0.1/src/StartApp.elm#L79-L117. There's no way to actually provide a type signature, let alone a monomorphic one, for the mailbox used in there.

[imeckler]

That is monomorphic in the type environment containing the type variable "action".

On Nov 11, 2015, at 07:41, Janis Voigtländer notifications@github.com wrote:

A problem with the proposal to require mailboxes to have monomorphic types: What do do about cases like the implementation of start in start-app/StartApp.elm? See https://github.com/evancz/start-app/blob/2.0.1/src/StartApp.elm#L79-L117. There's no way to actually provide a type signature, let alone a monomorphic one, for the mailbox used in there.

—

[jvoigtlaender]

I do know that one could make this monomorphic in the sense you mention, if one could write that down as a type annotation. But one cannot, given that Elm has no equivalent of Haskell's ScopedTypeVariables.

And when you cannot write it down, you do get it interpreted as a polymorphic type, and then suffer from the type unsoundness. Happened in the wild, see here.

[evancz]

Yay 0.17!