Hazel: A live functional programming environment featuring typed holes

mmastrac · a year ago

This is semi-related to one of the killer features of Eclipse that never really made it into any large-scale systems: the ability to run incomplete or broken code. The Eclipse Compiler for Java had a special feature that it could generate bytecode for nearly any file, including those that were utterly broken. It would mostly work, and you could incrementally work on unit tests alongside the code being developed.

It was honestly one of the most productive environments I ever worked in, and I'm somewhat sad nobody else has implemented this.

spockz · a year ago

Agda (2) has a similar feature called holes. Very similar to Haskell’s `nothing` and Scala’s `???`. The difference is that because of the dependently typedness the compiler can sometimes even fill in the code for you based on symbols in scope.

argiopetech · a year ago

Haskell has also had typed holes for several major versions now. Any underscore or name beginning with an underscore (to include values and types, unsure about kinds) gets an informative error message describing the type of the name, e.g.:

  Found hole `_' with type f (Free f b)

and relevant bindings, if applicable:

  Relevant bindings include
    >>= :: Free f a -> (a -> Free f b) -> Free f b
      (bound at holes.hs:28:3)
    f :: f (Free f a) (bound at holes.hs:29:8)
    g :: a -> Free f b (bound at holes.hs:29:14)
  In the first argument of `Free', namely `_'

Very useful for working your way out of a situation where the specific incantation to get to the right type isn't obvious.

Examples from [0].

[0] https://wiki.haskell.org/GHC/Typed_holes

fire_lake · a year ago

Isn’t this possible with any untyped language?

It does sound like a good feature though - very few languages have opt-out type checking. This is much better than opt-in IMO.

7h3kk1d · a year ago

Hazel will also run incomplete programs around holes. Most untyped languages will just crash as soon as something is incomplete.

conartist6 · a year ago

Yes and no. You need a universal way of saying "something that should exist here is missing"

ellis0n · a year ago

ACPUL works well even with partially broken code keeping programs free from crashes and freezes. Some functions were broken for a long time, but this didn’t block progress allowing me to complete 90% of important features and fix them after 10 years. This has been verified over time in practice. I believe even 30-50% of a program can work opening up many new possibilities.

kreyenborgi · a year ago

Haskell has something like this with -fdefer-type-errors: https://downloads.haskell.org/ghc/latest/docs/users_guide/ex...

    $ cat foo.hs
    something = to be done
    x = x + 1
    wat = x "¯\\_(ツ)_/¯"
    main = print "hi"
    
    
    $ ghc --make -O foo -fdefer-type-errors && echo sucesfuly compoiled && ./foo
    [1 of 1] Compiling Main             ( foo.hs, foo.o )
    
    foo.hs:2:13: warning: [-Wdeferred-out-of-scope-variables]
        Variable not in scope: to :: t1 -> t2 -> t
      |
    2 | something = to be done
      |             ^^
    
    foo.hs:2:16: warning: [-Wdeferred-out-of-scope-variables]
        Variable not in scope: be
      |
    2 | something = to be done
      |                ^^
    
    foo.hs:2:19: warning: [-Wdeferred-out-of-scope-variables]
        Variable not in scope: done
      |
    2 | something = to be done
      |                   ^^^^
    Linking foo ...
    sucesfuly compoiled
    "hi"
    $

argiopetech · a year ago

Haskell also has typed holes (with a similar -fdefer-typed-holes) since 7.10. I've described it in slightly more detail here in a previous post in this thread [0].

Typed holes (but not the defer- option) have been enabled by default for some time now. They're an immediate go-to when scratching my head over types. I prefer them to the type error output, not only because they give better suggestions, but also because they can be named (_a, _conversionFunction, etc).

[0] https://news.ycombinator.com/item?id=42016584

WantonQuantum · a year ago

I use IntelliJ now and I definitely miss this feature of Eclipse.

cies · a year ago

Why? What did you miss about it?

I'm asking as I prefer strict compilers that force me to handle all cases.

diegs · a year ago

And then you have Go, which won't even let you compile code with an unused variable...

Joker_vD · a year ago

    func TestWhatever(t *testing.T) {
        // ...lots of code

        _, _, _, _, _, _, _ = resp3, resp4, fooBefore, subFoo, bar2, barNew, zap2
    }

Like, I get it, it's a good feature, it caught quite a lot of typos in my code but can I please get an option to turn this checking off e.g. in unit tests? I just want to yank some APIs, look at their behaviour, and tinker a bit with the data.

tomcam · a year ago

I have never heard about this before. What exactly would happen to broken code? For example, would it skip the equivalent of the broken source line, or would it stub out a function altogether or what?

gmueckl · a year ago

I only used that feature inadvertently a long, long time ago. As I remember, the program would throw a Throwable exception when it would enter code that wasn't translatable. There was some sort of hot reloading, too. So you could try to fix the code and continue.

The really neat thing was that the Ecliose Java compiler is built specifically to support the IDE, so all the the warning and error annotations in the editor come from the actual compiler even while you are typing. There is no separate parser and linter just for the editor. I believe that the ability to translate broken source files on a best effort basis is actually an offshoot from that functionality.

mmastrac · a year ago

Literally that, it would throw exceptions with the compiler error. And as a sibling comment mentioned and I had forgotten -- it would allow for hotpatching code at runtime as you fixed compiler errors.

You could literally start the skeleton of a webserver and gradually add functionality to it without recompiling and it would mostly "just work". Certain changes would require the app to be restarted.

agumonkey · a year ago

embedded agile mode

agentultra · a year ago

Haskell has type holes. There are plugins that give you code actions to complete them, split case, etc. I love type holes.

Agda has them too and they're more powerful there: https://agda.readthedocs.io/en/latest/language/lexical-struc...

epolanski · a year ago

Typescript has a hole type too implemented in fp-ts and effect-ts.

Super useful for when you don't know what are you missing and get a type signature for it.

It's mostly useful for when you declare some `const foo: (bar: Bar) => Whatever` and in the midst of your implementation you don't know what you're missing.

Requires an advanced level in TS to be used to the max.

https://gcanti.github.io/fp-ts/modules/function.ts.html#hole

https://effect-ts.github.io/effect/effect/Function.ts.html#h...

disconcision · a year ago

there's this hacky quick way of partially emulating typed holes sans library too: https://dev.to/gcanti/type-holes-in-typescript-2lck

we (team hazel) recently used that device in our typescript version of a hazel setup for typed-hole-contextualized code completion as described in https://dl.acm.org/doi/10.1145/3689728

williamdclt · a year ago

I’m struggling to understand the use, do you have a concrete example?

cies · a year ago

For me Idris has best type holes.

dannyobrien · a year ago

Yes, and Idris actively encouraged iterative development that was based around its holes -- the book by Idris' creator Edwin Brady, Type-Driven Development[1], is an eye-opening introduction to this style of coding.

[1] - https://www.manning.com/books/type-driven-development-with-i...

disconcision · a year ago

happy to answer hazel questions; ive been working on hazel as cyrus' phd student for the last four years, and am currently working on moldable projectional interfaces for live programming in hazel. here are some of the things ive added to hazel: https://github.com/hazelgrove/hazel/pulls?q=is%3Apr+author%3...

and here's me speaking last week about using typed holes and the hazel language server to help provide code context for LLM code completion: https://www.youtube.com/watch?v=-DYe8Fi78sg&t=12707s

jakewins · a year ago

This is probably naive but: How does this differ from something like “declare a type, implement it with methods that all throw NotImplementedException”?

As in, is this “just” a less boilerplate-heavy version of that, or is it more capable?

7h3kk1d · a year ago

You can play with it at https://hazel.org/build/dev/ but programs don't "crash" when they're incomplete so "1 + 5 + ?" will evaluate to "6 + ?" in the editor. So your program can evaluate as far as possible with the holes. If you're using Java and throw NotImplementedException you lose all context to what did work.

conartist6 · a year ago

Nice to make your acquaintance! I've spent the last four years working on similar tech, though I'm not affiliated with any school or company. I've gone over to the Hazel implementation many times for inspiration and just to check in on the progress.

Here are some of the biggest questions I have:

Do you have any plans to bring editor gaps to languages other than Hazel?

Why is the Hazel editor first a text editor? E.g. it seems 100% happy to let a single poorly judged keystroke create an unbalanced brace or quote pair when it has much more semantically correct options for the next state it could generate...

P.S. Feel free to come check out BABLR: https://github.com/bablr-lang/, https://discord.gg/NfMNyYN6cX

disconcision · a year ago

good questions! both will be addressed soon with david moon's new tylr version (tylr being the underlying syntactic engine for hazel). the new tylr is designed to take a grammar as a parameter; we have a javascript grammar and a partial rust grammar, and are planning editor integrations. the new model also eschews the backpack (the yellow thing that contains matching delimiters) in lieu of inserting missing delimiters as 'ghosts' in a way that always shows the exact parse that the semantics engine is using, but also doesn't prevent typing normally. the current backpack solution is the result of trying to balance natural text editing with mandated syntactic correctness and it definitely has proved to have some rough edges... more on the new system soon

riffraff · a year ago

Congrats, this seems fun and neat!

But small question related to https://hazel.org/build/dev/, given

> Non-empty holes are the red boxes around type errors

... why is the case statement in the list example red-boxed?

7h3kk1d · a year ago

If you put the cursor on it you'll see an error message at the bottom. In this case the case expression is inexhaustive because it's only handling lists of size 0, 1, and 2.

nrabulinski · a year ago

(Haven’t worked with hazel and I couldn’t find much in the documentation so this may be wrong)

Because that case is non-exhaustive. It will match a list with 0, 1, or 2 elements, but the last arm matches a list with exactly 2 elements, not 2 or more, so as soon as you get to 3 or more elements, there’s no code to execute.

dang · a year ago

Related. Others?

Hazel: A live functional programming environment featuring typed holes - https://news.ycombinator.com/item?id=24299852 - Aug 2020 (14 comments)

Also:

Tylr: Demo of tile-based editing, a new kind of structure editing - https://news.ycombinator.com/item?id=27926758 - July 2021 (40 comments)

vosper · a year ago

I like the way the code examples work: A live editor with documentation that shows up on the right hand side (click the Play with Hazel) button.

But does it any more than a live editor and type checker? Can you actually create a program that does something?

disconcision · a year ago

we have ~ another year of basic type system and editor features prior to the 'doing something' phase. there are early-stage feature branches with stuff for web GUI programming & data science applications, but parts are awkward without in-progress basics like implicit polymorphism, a module system, and more sophisticated type inference.

sheepscreek · a year ago

Just came here to say that the editor UI is beautiful, works really well - even on mobile. Color me impressed.

jbjohns · a year ago

Interesting. I didn't notice any reference to Idris [1] but that was the first place I saw this style of development.

[1] https://www.youtube.com/watch?v=mOtKD7ml0NU

virtualritz · a year ago

I tried the playground on my Android phone and none of the key presses get through to the source code.

I can position the cursor by tapping and I get a virtual keyboard but I can't type anything.

Is this a bug or am I just missing something because If terrible UX?

disconcision · a year ago

its a bug. we should be clearer that we dont 'officially' support mobile yet (in that no-one regularly tests with it) but the no keyboard insertion thing is a chrome-specific issue (it works on firefox but there are other issues there)