Hazel: A live functional programming environment featuring typed holes

by deepakkarki • 2 years ago

234 86 2 years ago

vosper• 2 years 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?

disconcision7• 2 years 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.

aassddffasdf• 2 years ago

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

colonwqbang• 2 years ago

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

noelwelsh• 2 years ago

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.

aithrowawaycomm• 2 years ago

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.

wyager• 2 years ago

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

disconcision7• 2 years ago

yes. also keen on first class modules (coming soon to Hazel). syntax could have easily been more haskell-like, current team is pretty ecumenical wrt surface syntax, excepting that i have as yet been unable to convert anyone to the gospel of s-expressions.

biggest reason more haskelley syntax didnt/hasnt happen/ed is the current syntax engine does not support significant indentation. hazel concrete syntax isn't stable yet though we're also thinking seriously about semi-colons

dang• 2 years 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)

agentultra• 2 years 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...

epolanski2• 2 years 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...

williamdclt• 2 years ago

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

disconcision7• 2 years 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

cies3• 2 years ago

For me Idris has best type holes.

dannyobrien• 2 years 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...

davesnx• 2 years ago

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

mmastrac2• 2 years 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.

tomcam• 2 years 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?

gmueckl2• 2 years 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.

mmastrac2• 2 years 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.

WantonQuantum2• 2 years ago

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

cies3• 2 years ago

Why? What did you miss about it?

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

fire_lake• 2 years 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.

conartist64• 2 years ago

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

7h3kk1d4• 2 years ago

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

diegs• 2 years ago

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

Joker_vD3• 2 years 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.

kreyenborgi• 2 years 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"
    $

argiopetech2• 2 years 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

spockz• 2 years 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.

argiopetech2• 2 years 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

ellis0n• 2 years 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.

agumonkey• 2 years ago

embedded agile mode

disconcision7• 2 years 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

jakewins2• 2 years 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?

7h3kk1d4• 2 years 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.

riffraff• 2 years 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?

nrabulinski• 2 years 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.

7h3kk1d4• 2 years 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.

conartist64• 2 years 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

disconcision7• 2 years 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

sheepscreek• 2 years ago

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

hoistbypetard• 2 years ago

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• 2 years ago

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

keeganpoppen• 2 years ago

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

boogerlad• 2 years ago

How does this compare to lamdu?

ineil• 2 years ago

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?

virtualritz• 2 years 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?

disconcision7• 2 years 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)

jbjohns• 2 years 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

jlkuester7• 2 years ago

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!

7h3kk1d4• 2 years ago

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• 2 years ago

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.

imglorp• 2 years ago

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?

moomin• 2 years ago

The bindings are only valid for the expression following in.

Haskell does the same thing.

arthurbrown• 2 years ago

this is the syntax for variable binding in ocaml.

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

Hazel: A live functional programming environment featuring typed holes

Related Stories