Hazel: A live functional programming environment featuring typed holes

[mmastrac]

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]

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.

[fire_lake]

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.

[ellis0n]

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]

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"
    $

[WantonQuantum]

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

[diegs]

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

[tomcam]

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?

[agumonkey]

embedded agile mode

[agentultra]

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]

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...

[cies]

For me Idris has best type holes.

[disconcision]

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]

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?

[conartist6]

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

[riffraff]

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?

[dang]

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]

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]

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]

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

[jbjohns]

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]

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]

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)

[davesnx]

I always loved hazel, probably a great tool to teach. What has been build with it?

[hoistbypetard]

My first thought was the Mac app that's been around for about 18 years now:

https://www.noodlesoft.com

And it had a release today.

https://www.noodlesoft.com/release_notes

Seems rough to jump on a name that's been in continuous use for that long. Would it be hard to add another word to make it easier to disambiguate?

[nozzlegear]

My first thought when viewing your link was the name "Hazel" which has been around since the late 19th century or so. Couldn't the devs have chosen a different name or added another word?

Jokes aside, name collisions are bound to happen. These two apps seem entirely unrelated so I doubt anyone will accidentally install "Hazel, the Mac app for organizing folders and files" when they meant to use "Hazel, the live functional programming environment organized around type holes."

[imglorp]

Interesting syntax: all the "let" bindings end with "in", eg

    let comparison =
      (0 == 0, 0 < 1, 1 <= 1, 2 > 1, 1 >= 1) 
    in

Anyone know why "in" keyword?

[arthurbrown]

this is the syntax for variable binding in ocaml.

Hazel appears to be written in ocaml and mentions being "ml-like" on the site

[moomin]

The bindings are only valid for the expression following in.

Haskell does the same thing.

[keeganpoppen]

this seems like it's likely inspired by Idris, to which i say: awesome!

[jlkuester7]

Not sure if I have just spent too much time in the JS/TS world and so I have forgotten the pain in this area in proper compiled languages, but to me it seems like needing "typed holes" smells like maybe there is some abstraction missing in your codebase.

I prefer to have code layered in a way that my inflection points happen across well defined interfaces. Then I can make changes one layer at a time in increments that are small enough to still be able to reason about. But maybe I am totally mising the point of typed holes!

[7h3kk1d]

I'm not sure I understand your point. Typed holes aren't trying to get rid of the concept of interfaces or well designed abstractions. Rather they aim to help deal with incomplete programs that are still under development.

[mrkeen]

> maybe there is some abstraction missing

A hole is the answer to this question. You ask the compiler "what abstraction is missing?" and it tells you.

[boogerlad]

How does this compare to lamdu?

[ineil]

So if I’m told I have an A type personality and am also often called an A hole does that mean I can concatenate both to create the compound condition of having type holes?

[aassddffasdf]

Elm/ML is an interesting choice of mis-mash & a subtle slap in the face of Haskell? (Which on the surface is far more like Elm than ML is).

[aithrowawaycomm]

This seems like an attempt to stir up a flame war. Hazel is written in ReasonML and uses OCaml-style syntax, and the Elm influence is in the design of an interactive programming environment based on running the program as you edit it. I think they could have said SLIME/ML and conveyed a similar idea. I strongly doubt the authors have anything against Haskell.

[noelwelsh]

My reading is:

* Elm because Elm focused on making the language pleasant to use, and Hazel is in the same tradition of combining HCI + PL

* ML because Hazel is a strict / eager language, and people talk of ML family languages, of which Haskell is one.

So I don't think omitting Haskell is meant to be a slap in the face.

[colonwqbang]

I thought the same thing. "Hazel" sounds like a play on words, a "Hazy Haskell"? Or is it because hazels and elms are trees.

[wyager]

I would take that to mean "strict evaluation" and "simple type system"