Switching to NCurses?

62 views
Skip to first unread message

Joshua Hillerup

unread,
Feb 28, 2019, 10:18:05 PM2/28/19
to Idris Programming Language
So, I've been trying to add tabbed autocomplete to Blodwen's Repl for awhile now, and I've realized that the problem is that there's no way with the C libraries that Idris uses for interacting with the terminal to really do it properly.  Everywhere online seems to be suggesting using ncurses over the regular C standard libraries that the Idris C FFI uses, since the C standard doesn't really easily support unbuffered character input.  And what's more it really looks like it might have to be an all or nothing thing?

So, I've never been accused of being a C expert, so I'm quite possibly missing something here, but is my assumption correct, if I want unbuffered character input from the terminal I should be switching everything in Idris to ncurses?  And if so, would that be OK?  I don't want to go and put in the work and do a PR if it's not the direction we want Idris to go in for some reason.

Anyway, my biggest hope with this email is that someone will point out something simple I'm missing, and if so please let me know.  

Josh

Alex Queiroz

unread,
Mar 1, 2019, 2:18:44 AM3/1/19
to idris...@googlegroups.com
Hi,


On 1 Mar 2019, at 04:17, Joshua Hillerup <zen...@zenten.ca> wrote:


Anyway, my biggest hope with this email is that someone will point out something simple I'm missing, and if so please let me know.  


Have you seen `linenoise` yet? https://github.com/antirez/linenoise

Cheers,
Alex Silva

Leif Warner

unread,
Mar 1, 2019, 2:57:54 AM3/1/19
to idris...@googlegroups.com
There's a Haskell port of that: https://github.com/sdiehl/haskell-linenoise

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Edwin Brady

unread,
Mar 1, 2019, 4:37:55 AM3/1/19
to idris...@googlegroups.com
Hi Josh,
Great that you're doing this, thanks!

I don't have an answer to your question, but I do have one observation,
which is that if you're improving Blodwen's REPL, I think something that
might be worth trying instead of writing the REPL directly is
implementing a REPL via the IDE protocol, as a separate executable.

Partly I suggest this because I like the idea of separating the core
language implementation from the interactive features (and I think
that's what David had in mind early on when designing the protocol).
And, if anyone has any thoughts about other ways of writing a REPL, e.g.
a graphical interface, or something even more imaginative - Smalltalk
inspired perhaps - they'll have a good place to start.

But also, more practically, it means that if I ever get around to
porting the Blodwen code so that it can compile itself (this is the
thing I'd call Idris 2) then there's more chance of having a ready made
REPL for it that already works.

Edwin

Joshua Hillerup

unread,
Mar 1, 2019, 6:07:29 AM3/1/19
to idris...@googlegroups.com
I had tried that before but ended up actually stopping work on that project when I heard about Blodwen. I can certainly pick back up again though.

Joshua Hillerup

unread,
Mar 1, 2019, 6:14:45 AM3/1/19
to idris...@googlegroups.com
So, one question, what do people think would be a good way to to have shared code between my project and Blodwen, for things like the wire protocol? I think doing that and keeping it in GitHub makes a lot more sense than manually copying and pasting, or manually implementing the same protocol twice.

Alex Queiroz

unread,
Mar 1, 2019, 6:18:55 AM3/1/19
to idris...@googlegroups.com
Hi,


On 1 Mar 2019, at 12:14, Joshua Hillerup <zen...@zenten.ca> wrote:

So, one question, what do people think would be a good way to to have shared code between my project and Blodwen, for things like the wire protocol? I think doing that and keeping it in GitHub makes a lot more sense than manually copying and pasting, or manually implementing the same protocol twice.


But the point of having a protocol is to be able to separate things, no? You can develop your project in its own repository, using whichever programming language you prefer and, if it conforms to the IDE protocol, it will be interoperable with Blodwen.

Joshua Hillerup

unread,
Mar 1, 2019, 6:21:01 AM3/1/19
to idris...@googlegroups.com
Yes, the implementation should be different. But if both the client and server are written in Idris there would be a big advantage to having the types/interface that define the protocol be shared, no?

David Thrane Christiansen

unread,
Mar 1, 2019, 12:09:53 PM3/1/19
to idris...@googlegroups.com
Hi all,

> Partly I suggest this because I like the idea of separating the core language implementation from the interactive features (and I think that's what David had in mind early on when designing the protocol). And, if anyone has any thoughts about other ways of writing a REPL, e.g. a graphical interface, or something even more imaginative - Smalltalk inspired perhaps - they'll have a good place to start.

The protocol design isn't really something that I can claim credit for
- it's basically just a dialect of Swank, the protocol that's been
used by SLIME and DIME since I was an undergrad back in Idaho in the
early 2000s. Hannes Mehnert adapted it to the operations that make
sense in Idris as opposed to Lisp. But this is definitely the kind of
use cases that it was designed for.

It may be instructive to take a look at the native REPLs in various
Lisps. They're usually quite unpleasant to actually use - SBCL for
instance doesn't even have readline available by default, because it's
really intended to be used as a server for a nice UI that lives
elsewhere.

> Yes, the implementation should be different. But if both the client and server are written in Idris there would be a big advantage to having the types/interface that define the protocol be shared, no?

Yes, I think that a lot of the code could be shared, so it definitely
makes sense to have the communications part of the protocol be
implemented as a library in Idris. You can probably start by
extracting the relevant part from Blodwen itself, and then having
Blodwen and your REPL both depend on the library.

If you want to write this fancy REPL in something other than Idris, it
may be worth looking at Brick, a library that one of my colleagues
made for making fancy full-screen text UIs in Haskell with an API
that's much easier to use than Curses. Then, you could extract the
Haskell implementation of the IDE protocol from Idris itself into a
library to share. This could be used to make something as cool as
bpython (https://bpython-interpreter.org/screenshots.html).

Another thing worth considering is whether a terminal emulator is the
best interface here, or whether it would be easier to get a nice UI
using a real GUI library. That makes it easier to do things like
context menus, tooltips, pictures, links, etc. Despite the
old-fashioned look at feel, it's worth looking at
https://www.youtube.com/watch?v=kfBmRsPRdGg for some of what is
possible. The current Emacs interface to the Idris REPL also has some
nice features, like semantic highlighting of the user's input
expression, clickable interactive output, tooltips, expandable trees
to explore the result of "who calls" queries, etc.

My goal here is not to overwhelm you! Old-fashioned command-line REPLs
with completion are certainly useful, and one of them for Blodwen
would be great. There's just no reason to limit your creativity to
what ghci (or idris-mode for emacs) does.

Have fun, and please let me know if I can answer questions about the
IDE protocol.

David

Ara Adkins

unread,
Mar 1, 2019, 2:31:23 PM3/1/19
to idris...@googlegroups.com
Is there any thought to basing Blodwen’s IDE protocol on the Language Server Protocol instead? It’d allow for much more flexible integrations into many editors.

_ara

David Thrane Christiansen

unread,
Mar 1, 2019, 5:06:37 PM3/1/19
to idris...@googlegroups.com
Hi Ara,

I don't know what's planned for Blodwen, but I'll share some
perspective as a major implementor of current-Idris's editor
interactions.

While Idris's editor integration predates the VS Code LSP, I still
think I'd be hesitant about adopting it. In order to get the kind of
experience that I wanted to have, it would require lots and lots of
extensions, to the point where it's not really fair to say that one is
using the same protocol. LSP has features that Idris doesn't, which is
fine, but Idris also has lots of features not covered by LSP. While
LSP is a reasonable floor to get the very basic stuff working quickly,
it seems to be also setting a ceiling for everyone's ambitions these
days.

Here's some examples of where they don't match well:

* LSP specifies that text is sent as only plain text or Markdown.
Idris supports rich semantic annotations on text from the compiler,
giving things like doc summaries, type signatures, and handles that
can be used for interaction with the underlying information
represented by the string. Consequences of this are the semantic
highlights, the ability to have interactive examples in docs (e.g,
right-click on the example to get it evaluated in place), and
interactive error messages. It'd be a shame to give those things up.

* LSP doesn't have any notion of "holes" in a program, but getting the
hole list is an important part of type-driven editing.

* LSP still doesn't have a way for the compiler to highlight the
source document based on the semantics of each substring. It's not
clear that there even is one protocol for that that's reasonable for
different languages - Idris sends highlighting as a "push" as a side
effect of type checking, while other languages may work better if the
editor "pulls" highlighting when scrolling around.

* LSP hard-codes UI features of VS Code, like "code lens" and "hover",
rather than talking about the meaning of documents. The Idris protocol
instead has things like "what is the type" and "what are the docs".
This is a place where Idris's protocol enables a wider variety of UIs.
This is a way in which LSP is significantly less flexible. Imagine if
the Idris protocol hardcoded imenu and the Emacs minibuffer!

* LSP doesn't contain commands for REPLs, nor for things like case-splitting.

There's a bunch more. It would be reasonable to define lots of
extensions to "LSP" to get back up to where the current Idris UIs are,
but these would still require lots of implementation in each editor. I
think the big benefit of using the VS Code protocol would be that an
extremely basic experience would be quickly available, but almost all
the work is in the parts that go beyond what LSP offers anyway. The
other big benefit is that LSP wants compilers to be structured in a
certain way, and I think that redoing Idris/Blodwen in that way would
be an improvement. I'd almost rather see a better protocol for
languages like Idris, Agda, and Lean that could be supported directly.

If those extensions ever do get made to LSP, it'd be straightforward
to retarget at least the Emacs mode. Most of the code is not
particularly tied to the protocol - it's about displaying appropriate
UIs and such.

David

Ara Adkins

unread,
Mar 2, 2019, 7:55:03 AM3/2/19
to idris...@googlegroups.com
Hi David,

Thank you so much for all that insight! It not only answers my question, but actually gives me a great wealth of experience to think about - I’ve actually got the implementation of an IDE protocol on my plate for the near future.

You’ve pretty much echoed my thinking for my task that LSP would need a lot of extensions to support everything needed by the language I’m working on, particularly the provision of rich additional semantic data.

Do you mind if I email you off this list to pick your brain about the topic?

Best
_ara

David Thrane Christiansen

unread,
Mar 2, 2019, 12:02:27 PM3/2/19
to idris...@googlegroups.com
Hi Alea,

Time permitting, I'm happy to answer emails :-)

David

David Thrane Christiansen

unread,
Mar 2, 2019, 12:03:30 PM3/2/19
to idris...@googlegroups.com
Sorry for sending a name autocorrect result, Ara.

Raingloom

unread,
Mar 3, 2019, 4:09:51 AM3/3/19
to idris...@googlegroups.com
Hey everyone

> Another thing worth considering is whether a terminal emulator is the
> best interface here, or whether it would be easier to get a nice UI
> using a real GUI library. That makes it easier to do things like
> context menus, tooltips, pictures, links, etc. Despite the
> old-fashioned look at feel, it's worth looking at
> https://www.youtube.com/watch?v=kfBmRsPRdGg for some of what is
> possible. The current Emacs interface to the Idris REPL also has some
> nice features, like semantic highlighting of the user's input
> expression, clickable interactive output, tooltips, expandable trees
> to explore the result of "who calls" queries, etc.

What about a Jupyter kernel? Haskell has one but I could never get it to compile so I haven't tried it out.
Reply all
Reply to author
Forward
0 new messages