5 ms·

Type hole-based programming is not only available is dependently-typed languages. It's also available in Haskell and even Ocaml, although it's not quite as help

Type hole-based programming is not only available is dependently-typed languages. It's also available in Haskell and even Ocaml, although it's not quite as helpful as in Agda (since you can't type-hole value types, obviously): https://wiki.haskell.org/GHC/Typed_holes https://wiki.haskell.org/GHC/Typed_holes Even OCaml can kind of simulate type holes: https://www.reddit.com/r/ocaml/comments/2ulom8/a_trick_for_simulating_typed_holes_in_ocaml/ https://www.reddit.com/r/ocaml/comments/2ulom8/a_trick_for_s... Purescript has nice IDE integration and type holes (Haskell likely has something similar, not sure): https://qiita.com/kimagure/items/f1827c9129f3ee6ede35#type-holes https://qiita.com/kimagure/items/f1827c9129f3ee6ede35#type-h...

pezo1919 7y ago
Ah, I did not know that! The Purescript integration seems definitely interesting! Do you use these tools for work?
- jnbiche 7y ago
  I've used type holes in my work, frequently. But I've not yet used Purescript or Purescript's language server professionally, although I hope to get a chance to do so eventually. To be honest, Haskell and OCaml (which I have used at work) have similar language servers available for IDE integration, but I'm a vim user and tend to use plain Vim along with an open REPL (making use of type holes in the REPL). But I've been meaning to explore the IDE integrations of Haskell and OCaml as well as Purescript.
  - namibj 7y ago
    I think I got that in the form of type-aware auto completion in Atom with Haskell. It might be partially limited, but I'm not sure. It was rather flaky due to version missmatch between GHC and the language server. It's pretty awesome.
    - pezo1919 7y ago
      Ah I have just realized it might be "just a classic typed language IDE" experience and Dependent Types seems just way above. Am I missing something?
      - namibj 7y ago
        Yes. Dependent typed tell you that the vector you pass along the matrix to a matrix-vector-multiply has to be one with not just the right datatype, but also the right size. It could also suggest (postfix w.r.t. the container type) operators with better performance for the container's known size (range). Or, depending on previous conditionals, filter postfix operators you apply to a field of a datastructure, if that field is constrained by the condition branching on another field in the datastructure. I.e., applying a specific operator to a conditional sum type that's no longer a sum type if another variable / field is restricted beyond it's datatype (a range of integers, an enum value, a theoretical utf-8 string previously restricted to ASCII, etc.).

pezo1919 7y ago

Ah, I did not know that! The Purescript integration seems definitely interesting! Do you use these tools for work?

jnbiche 7y ago
I've used type holes in my work, frequently. But I've not yet used Purescript or Purescript's language server professionally, although I hope to get a chance to do so eventually. To be honest, Haskell and OCaml (which I have used at work) have similar language servers available for IDE integration, but I'm a vim user and tend to use plain Vim along with an open REPL (making use of type holes in the REPL). But I've been meaning to explore the IDE integrations of Haskell and OCaml as well as Purescript.
- namibj 7y ago
  I think I got that in the form of type-aware auto completion in Atom with Haskell. It might be partially limited, but I'm not sure. It was rather flaky due to version missmatch between GHC and the language server. It's pretty awesome.
  - pezo1919 7y ago
    Ah I have just realized it might be "just a classic typed language IDE" experience and Dependent Types seems just way above. Am I missing something?
    - namibj 7y ago
      Yes. Dependent typed tell you that the vector you pass along the matrix to a matrix-vector-multiply has to be one with not just the right datatype, but also the right size. It could also suggest (postfix w.r.t. the container type) operators with better performance for the container's known size (range). Or, depending on previous conditionals, filter postfix operators you apply to a field of a datastructure, if that field is constrained by the condition branching on another field in the datastructure. I.e., applying a specific operator to a conditional sum type that's no longer a sum type if another variable / field is restricted beyond it's datatype (a range of integers, an enum value, a theoretical utf-8 string previously restricted to ASCII, etc.).