3 ms·

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

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.
      - dietr1ch 2y ago
        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 2y ago
    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 2y ago
  there's this hacky quick way of partially emulating typed holes sans library too: https://dev.to/gcanti/type-holes-in-typescript-2lck 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 https://dl.acm.org/doi/10.1145/3689728
cies 2y ago
For me Idris has best type holes.
- dannyobrien 2y ago
  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-idris https://www.manning.com/books/type-driven-development-with-i...

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.
    - dietr1ch 2y ago
      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 2y ago
  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 2y ago
there's this hacky quick way of partially emulating typed holes sans library too: https://dev.to/gcanti/type-holes-in-typescript-2lck 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 https://dl.acm.org/doi/10.1145/3689728

cies 2y ago

For me Idris has best type holes.

dannyobrien 2y ago
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-idris https://www.manning.com/books/type-driven-development-with-i...