[HN Gopher] Hazel: A live functional programming environment fea...
___________________________________________________________________
Hazel: A live functional programming environment featuring typed
holes
Author : deepakkarki
Score : 222 points
Date : 2024-10-31 06:57 UTC (1 days ago)
(HTM) web link (hazel.org)
(TXT) w3m dump (hazel.org)
| vosper wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| I would take that to mean "strict evaluation" and "simple type
| system"
| disconcision wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| I'm struggling to understand the use, do you have a concrete
| example?
| dietr1ch wrote:
| 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
| LandR wrote:
| This is awesome, but I find that syntax so hard to
| follow, but that's just me being unfamiliar with it I
| guess.
| dietr1ch wrote:
| It happens, but all syntax families eventually become
| familiar, even on LISP you eventually stop worrying about
| the parentheses as you learn how to grok the code.
| epolanski wrote:
| Suppose you declare some:
|
| const transformFoo: (foos: Foo[]) => Bar
|
| and you start implementing it and get stuck with some
| callback or whatever you can put a `hole` and it will tell
| you the type signature of what you're missing.
| disconcision wrote:
| 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
| cies wrote:
| For me Idris has best type holes.
| dannyobrien wrote:
| 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 wrote:
| I always loved hazel, probably a great tool to teach. What has
| been build with it?
| mmastrac wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| That sounds like an incredibly useful feature. Do you
| recall what version you were using?
| gmueckl wrote:
| 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.
| jakewins wrote:
| Well, regression in _that_ feature set, but it's better
| in other features, many of which drove people off of
| Eclipse.
|
| When it worked, it was really, really good, agree. My
| experience was that it usually didn't though, swap
| branches a few times and the caches would be broken, time
| for "invalidate caches and restart". Multiple times per
| week, each time it'd take an hour to re-index.. that was
| a lot of time we got back again when we switched to
| IntelliJ
| ryukoposting wrote:
| This sounds like the sort of feature that will show up in
| a "vintage software" youtube video essay in a few years.
| I kinda want to go find it and give it a whirl.
| veqq wrote:
| Common Lisp's REPL works like this.
| mmastrac wrote:
| 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.
| cies wrote:
| CRTL-SHIFT-F9 (IntelliJ) works for me on most Java and
| Kotlin code in IntelliJ, as long as no method/class
| signatures are changed.
| WantonQuantum wrote:
| I use IntelliJ now and I definitely miss this feature of
| Eclipse.
| cies wrote:
| Why? What did you miss about it?
|
| I'm asking as I prefer strict compilers that force me to
| handle all cases.
| WantonQuantum wrote:
| Generally, it's a very pragmatic thing like being able to
| quickly run something to make sure it's working but some
| other part of the code is temporarily broken because I'm
| currently changing things and don't care that that part is
| currently broken. In IntelliJ I have to stop doing what I'm
| currently thinking about and go over to that other part of
| the code and comment out some things or otherwise fix it up
| (usually in a way that won't be permanent because it's
| broken for a reason) before I can run the code I'm working
| on.
|
| In an ideal world, the codebase would be modular and
| testable and all those good things but I work in a large
| enterprise dev team and some of the codebase is many (many)
| years old and it's no longer feasible to refactor it into
| anything like what would be needed to allow the code to be
| modularized in such a way that would obviate the necessity
| to do the above.
| foota wrote:
| I don't think they want to have thing broken in the steady
| state, but anything that relies on things building for
| analysis etc.,. Could benefit from this.
| fire_lake wrote:
| 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.
| conartist6 wrote:
| Yes and no. You need a universal way of saying "something
| that should exist here is missing"
| 7h3kk1d wrote:
| Hazel will also run incomplete programs around holes. Most
| untyped languages will just crash as soon as something is
| incomplete.
| instig007 wrote:
| Laziness would be enough for this case, Haskell will
| happily run your programs around _undefined_
| diegs wrote:
| And then you have Go, which won't even let you compile code
| with an unused variable...
| Joker_vD wrote:
| 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.
| TwentyPosts wrote:
| All of this could've been prevented if Go just had two ways
| to compile. Debug and release.
|
| The go devs decided against this since they didn't want to
| build a highly optimizing (read: slow) compiler, but that
| is missing the point of developer ergonomics.
| umanwizard wrote:
| It could be prevented in an even simpler way: emitting
| warnings.
|
| Most people nowadays ban building with warnings in CI and
| allow them during local development. But "CI" was barely
| a thing when go was developed so they just banned them
| completely. And now they are probably too stubborn to
| change.
| umanwizard wrote:
| The good news is if you use Nix or Guix it's relatively
| easy to hack your local build of the compiler to demote the
| unused variables hard error to just a warning.
| okwhateverdude wrote:
| You know, for some weird reason, it never crossed my mind
| to hack the Go compiler to let me do things like that.
| And it's such a great idea.
| umanwizard wrote:
| This patch is working for me. Good luck!
|
| https://gist.github.com/umanwizard/9793393083a42db933579f
| e21...
| politician wrote:
| This example isn't particularly good code. If you've got
| "lots of code" that names a bunch of variables (e.g. using
| ':=') that are never referenced AND you have a good reason
| not to do so (which I doubt: given this context it looks
| like an incomplete test), then predeclare these 'excess'
| variables: func TestWhatever(t *testing.T)
| { var resp3, resp4, fooBefore, subFoo, bar2,
| barNew, zap2 theirType // ...lots of code
| }
|
| Alternatively, use '_' where they are being defined:
| // instead of resp2, err := doit() //
| use _, err := doit()
|
| If, and given this context it's likely, you're checking
| these errors with asserts, then either change the name of
| the error variable, predeclare the err name (`var err
| error`), or split it into multiple tests instead of one
| giant spaghetti super test.
|
| That said, in a code review, at a minimum, I would probably
| ask that these variables be checked for nil/default which
| would completely eliminate this problem.
| kreyenborgi wrote:
| 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 "-\\_(tsu)_/-" 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 wrote:
| 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 wrote:
| 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 wrote:
| 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
| jimbokun wrote:
| Could this be used to build an editor for Haskell like the
| one for Hazel?
| ellis0n wrote:
| 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 wrote:
| embedded agile mode
| disconcision wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| (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.
| 7h3kk1d wrote:
| 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.
| conartist6 wrote:
| 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 wrote:
| 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 wrote:
| Just came here to say that the editor UI is beautiful, works
| really well - even on mobile. Color me impressed.
| hoistbypetard wrote:
| 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 wrote:
| 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 wrote:
| this seems like it's likely inspired by Idris, to which i say:
| awesome!
| boogerlad wrote:
| How does this compare to lamdu?
| ineil wrote:
| 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 wrote:
| 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?
| jbjohns wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| > 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 wrote:
| 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 wrote:
| The bindings are only valid for the expression following in.
|
| Haskell does the same thing.
| arthurbrown wrote:
| this is the syntax for variable binding in ocaml.
|
| Hazel appears to be written in ocaml and mentions being "ml-
| like" on the site
___________________________________________________________________
(page generated 2024-11-01 23:01 UTC)