11 ms·

Hazel: A live functional programming environment featuring typed holes

234 points by deepakkarki 2y ago

vosper 2y 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 2y 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 2y 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 2y 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 2y 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 2y 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 2y ago
  I would take that to mean "strict evaluation" and "simple type system"
  - disconcision 2y 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 2y ago
Related. Others? Hazel: A live functional programming environment featuring typed holes - https://news.ycombinator.com/item?id=24299852 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 https://news.ycombinator.com/item?id=27926758 - July 2021 (40 comments)
agentultra 2y 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-structure.html#holes https://agda.readthedocs.io/en/latest/language/lexical-struc...
- epolanski 2y 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://gcanti.github.io/fp-ts/modules/function.ts.html#hole https://effect-ts.github.io/effect/effect/Function.ts.html#hole https://effect-ts.github.io/effect/effect/Function.ts.html#h...
  - williamdclt 2y ago
    I’m struggling to understand the use, do you have a concrete example?
    - dietr1ch 2y ago
      Brady has a presentation about Idris where he shows Type-Driven development (where you write code that could typecheck with some holes and you get the compiler to help you figure out the missing types for your "whatever/something" untyped variables) https://youtu.be/X36ye-1x_HQ?t=5m15s https://youtu.be/X36ye-1x_HQ?t=5m15s
      - LandR 2y ago
        This is awesome, but I find that syntax so hard to follow, but that's just me being unfamiliar with it I guess.
davesnx 2y ago
I always loved hazel, probably a great tool to teach. What has been build with it?
mmastrac 2y 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 2y 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 2y 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.
    - ryukoposting 2y ago
      That sounds like an incredibly useful feature. Do you recall what version you were using?
      - gmueckl 2y ago
        I believe that Eclipse 2.x already had most of these features, but it certainly was in almost all 3.x versions as far as I remember. That IDE was amazingly far ahead of its time. Even 20 years later, tools like VS Code feel like a shocking regression in capabilities to me.
disconcision 2y 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%3Adisconcision 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 https://www.youtube.com/watch?v=-DYe8Fi78sg&t=12707s
- jakewins 2y 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 2y ago
    You can play with it at https://hazel.org/build/dev/ 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 2y ago
  Congrats, this seems fun and neat! But small question related to https://hazel.org/build/dev/ 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 2y 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.
sheepscreek 2y ago
Just came here to say that the editor UI is beautiful, works really well - even on mobile. Color me impressed.
hoistbypetard 2y ago
My first thought was the Mac app that's been around for about 18 years now: https://www.noodlesoft.com https://www.noodlesoft.com And it had a release today. https://www.noodlesoft.com/release_notes 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 2y 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 2y ago
this seems like it's likely inspired by Idris, to which i say: awesome!
boogerlad 2y ago
How does this compare to lamdu?
ineil 2y 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 2y 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 2y 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 2y 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 https://www.youtube.com/watch?v=mOtKD7ml0NU
jlkuester7 2y 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!
- 7h3kk1d 2y 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 2y 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 2y 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 2y ago
  The bindings are only valid for the expression following in. Haskell does the same thing.
- arthurbrown 2y 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

234 points by deepakkarki 2y 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 2y 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 2y 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 2y 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 2y 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 2y 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 2y ago
I would take that to mean "strict evaluation" and "simple type system"
- disconcision 2y 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 2y ago

Related. Others? Hazel: A live functional programming environment featuring typed holes - https://news.ycombinator.com/item?id=24299852 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 https://news.ycombinator.com/item?id=27926758 - July 2021 (40 comments)

agentultra 2y 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-structure.html#holes https://agda.readthedocs.io/en/latest/language/lexical-struc...

epolanski 2y 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://gcanti.github.io/fp-ts/modules/function.ts.html#hole https://effect-ts.github.io/effect/effect/Function.ts.html#hole https://effect-ts.github.io/effect/effect/Function.ts.html#h...
- williamdclt 2y ago
  I’m struggling to understand the use, do you have a concrete example?
  - dietr1ch 2y ago
    Brady has a presentation about Idris where he shows Type-Driven development (where you write code that could typecheck with some holes and you get the compiler to help you figure out the missing types for your "whatever/something" untyped variables) https://youtu.be/X36ye-1x_HQ?t=5m15s https://youtu.be/X36ye-1x_HQ?t=5m15s
    - LandR 2y ago
      This is awesome, but I find that syntax so hard to follow, but that's just me being unfamiliar with it I guess.

davesnx 2y ago

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

mmastrac 2y 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 2y 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 2y 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.
  - ryukoposting 2y ago
    That sounds like an incredibly useful feature. Do you recall what version you were using?
    - gmueckl 2y ago
      I believe that Eclipse 2.x already had most of these features, but it certainly was in almost all 3.x versions as far as I remember. That IDE was amazingly far ahead of its time. Even 20 years later, tools like VS Code feel like a shocking regression in capabilities to me.

disconcision 2y 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%3Adisconcision 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 https://www.youtube.com/watch?v=-DYe8Fi78sg&t=12707s

jakewins 2y 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 2y ago
  You can play with it at https://hazel.org/build/dev/ 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 2y ago
Congrats, this seems fun and neat! But small question related to https://hazel.org/build/dev/ 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 2y 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.

sheepscreek 2y ago

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

hoistbypetard 2y ago

My first thought was the Mac app that's been around for about 18 years now: https://www.noodlesoft.com https://www.noodlesoft.com And it had a release today. https://www.noodlesoft.com/release_notes 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 2y 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 2y ago

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

boogerlad 2y ago

How does this compare to lamdu?

ineil 2y 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 2y 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 2y 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 2y 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 https://www.youtube.com/watch?v=mOtKD7ml0NU

jlkuester7 2y 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!

7h3kk1d 2y 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 2y 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 2y 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 2y ago
The bindings are only valid for the expression following in. Haskell does the same thing.
arthurbrown 2y 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