Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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



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


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


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


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


This is awesome, but I find that syntax so hard to follow, but that's just me being unfamiliar with it I guess.


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.


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.


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




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: