It was honestly one of the most productive environments I ever worked in, and I'm somewhat sad nobody else has implemented this.
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].
It does sound like a good feature though - very few languages have opt-out type checking. This is much better than opt-in IMO.
$ 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"
$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).
I'm asking as I prefer strict compilers that force me to handle all cases.
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.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.
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.
Agda has them too and they're more powerful there: https://agda.readthedocs.io/en/latest/language/lexical-struc...
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...
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
[1] - https://www.manning.com/books/type-driven-development-with-i...
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
As in, is this “just” a less boilerplate-heavy version of that, or is it more capable?
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
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?
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.
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)
But does it any more than a live editor and type checker? Can you actually create a program that does something?
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?
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?
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."
let comparison =
(0 == 0, 0 < 1, 1 <= 1, 2 > 1, 1 >= 1)
in
Anyone know why "in" keyword?Hazel appears to be written in ocaml and mentions being "ml-like" on the site
Haskell does the same thing.
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!
A hole is the answer to this question. You ask the compiler "what abstraction is missing?" and it tells you.
* 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.
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