Protocol definition

[gracjan]

Requirements:

1. Follows generally accepted json practices.
2. Outside languages are untyped, so is json.
3. Works in async manner.
4. Enables easy error handling on Editor's side.

There seems to be a consensus that we would like to use some hints for types in the json itself, we can base a simple idea roughly on inverse of Type-indexed rows.

Lets define a set of possible responses as an open sum with following examples:

{"error": {"ui_message": ..., "code": ...}}
{"type_info": {"type":"IO () -> IO ()"}}
{"diff": {"XYZ.hs" : { diff description}}
{"plugins": {"p1": {?}, "p2": {?}}
... more follow

this translates to Haskell data declarations:

data Error = Error { ui_message :: Text, code :: Int }
instance ValidResponse Error where ...
data TypeInfo = TypeInfo { typem :: Text }
instance ValidResponse TypeInfo where ...
data Diff = Diff { diff :: ??? }
instance ValidResponse Diff where ...
data Plugins = Plugins { plugins :: ??? }
instance ValidResponse Plugins where ...
...etc

Rationale:

1. On the editors side there is no confusion when using labels: response.type_info.type
2. On Haskell side label name map one to one with type (on the same level of nesting in json).
3. Error handling on editors side is pretty easy, just handle one case "error".
4. When there is a lack of error handling on editors side there is no confusion (right now "contents" may be valid response or error string, only known after inspecting "tag")

[JPMoresmau]

I fear that having specific types like that links them very much to a specific command. So then plugin authors will either abuse these types, or put everything into the most generic response type they can find.
Your example seem to always imply that the content of each tag is an object, like in

{"type_info": {"type":"IO () -> IO ()"}}

But really in that example, having an object brings nothing over the string

{"type_info": "IO () -> IO ()"}

What would be so bad having the type command returning

 {"string": "IO () -> IO ()"}

For example?

[gracjan]

@JPMoresmau: very good question.

I think that the index key should answer the question: what is supposed to happen to the value? There supposedly is a function in editor that knows what to do with type information, another one that knows what to do with messages, but there is none that knows what to do with a generic string.

[alanz]

My mental hook on this is "widget".

The initial tag tells the editor what kind of processing to do on the rest, in terms of presentation on the UI.

We should be able to come up with a small set of meaningful widgets/semantic verbs, which can then be implemented in any IDE supporting HIE

[JPMoresmau]

Is it our job to mandate what should an editor do with what we return? An editor can display a string as a tooltip or since it knows it's the return of the type command, parse it as a type signature and display it in a tree structure, adding documentation on each type encountered in the signature, etc. An editor may request the type of an expression to display to the user, or to do something invisible (update a metadata lookup table).
I think there is value in having some type information ("this is not a simple string, this is a type signature"), but we're also adding complexity here. I have another example; in the Atom editor, with ghc-mod integration, you can ask for "info" or "type" on an expression. The editor does the same thing: show the resulting string in a tooltip. But there are two different types of "string". If we type precisely everything, then the code in the editor will need to be different in each case (not extracting the same field from the JSON). I know it's not a huge difference, but it's another burden on the editor developer.

[alanz]

It is not mandating what to do so much as indicating what the thing is in terms that make sense in the context of providing a UI

[JPMoresmau]

OK fine. And plugin writers will then be able to add their own types, and editors will have to support these?

[alanz]

The process of extending the "blessed" types is unclear to me.

I think it is something that should happen via a considered process, as it potentially has a wide impact.

[JPMoresmau]

Why? I've developed a tool that could be useful for editors, so I write a hie plugin. I return a complex structure, encoded as a type in Haskell and represented as a JSON object, etc on the wire. Editors either don't support my plugin and will not use its commands, or will support it and will have to know how to handle my return structure. Who else needs to bless my return type?

[alanz]

I think to start with we should let it run as you say, we just need to be careful that we do not end up with a multitude of types that are not quite the same, so the burden on IDE integrators becomes high.

It should be self-regulating in the sense that if a plugin writer wants a feature to be widely used quickly they should reuse one of the exiting types known by the IDEs at that point

[alanz]

Just for reference

• https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/IdeMode.hs
• http://docs.idris-lang.org/en/latest/reference/ide-protocol.html

[JPMoresmau]

000032(:return (:ok "Loaded /home/hannes/empty.idr") 1)

So I think we need a simple {"ok":"string"} result. More complex structures can be typed. That seems to me to be a good compromise.

[gracjan]

The full example is:

00002a((:load-file "/home/hannes/empty.idr") 1)
000039(:write-string "Type checking /home/hannes/empty.idr" 1)
000025(:set-prompt "/home/hannes/empty" 1)
000032(:return (:ok "Loaded /home/hannes/empty.idr") 1)

Then :ok needs to be interpreted as output code of the :load-file command. Note that :load-file does not return any additional information except that it succeeded loading empty.idr.

I see many commands that return only success/failure to share the :ok response type, but then interpretation of the string in idris-mode explicitly to use it as advise and nothing else.

[cocreature]

Our protocol has become reasonably stable, so I would prefer to open more concrete issues for any issues we still have or find in the future instead of this general one. Everyone fine with that?

[cocreature]

Closing, please reopen more specific issues if you find things we need to fix or change.