Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Hazel: A live functional programming environment featuring typed holes

hazel.org

Post reply on HN
Print view View original

51–60 of 88 posts

Re: Hazel: A live functional programming environment featuring typed holes

#51

Post by 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!

Re: Hazel: A live functional programming environment featuring typed holes

#52

Post by dannyobrien »

cies wrote: post #23
agentultra wrote: post #8

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

For me Idris has best type holes.

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

Re: Hazel: A live functional programming environment featuring typed holes

#53

Post by argiopetech »

spockz wrote: post #45
mmastrac wrote: post #10

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 w…

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.

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

Re: Hazel: A live functional programming environment featuring typed holes

#54

Post by argiopetech »

kreyenborgi wrote: post #41
mmastrac wrote: post #10

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 w…

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 -> t…

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

Re: Hazel: A live functional programming environment featuring typed holes

#55

Post by 7h3kk1d »

fire_lake wrote: post #27
mmastrac wrote: post #10

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 w…

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.

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

Re: Hazel: A live functional programming environment featuring typed holes

#56

Post by 7h3kk1d »

jakewins wrote: post #39
disconcision wrote: post #19

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 co…

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?

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.

Re: Hazel: A live functional programming environment featuring typed holes

#57

Post by 7h3kk1d »

riffraff wrote: post #43
disconcision wrote: post #19

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 co…

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?

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.

Re: Hazel: A live functional programming environment featuring typed holes

#58

Post by TwentyPosts »

Joker_vD wrote: post #37
diegs wrote: post #28

Earlier quoted context omitted.

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

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.

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.

Re: Hazel: A live functional programming environment featuring typed holes

#59

Post by 7h3kk1d »

jlkuester7 wrote: post #51

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 tha…

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.

Re: Hazel: A live functional programming environment featuring typed holes

#60

Post by ellis0n »

mmastrac wrote: post #10

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 w…

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.
Post reply on HN