6 ms·

Your post is very vague, but Agda and Coq use types to help you gradually write definitions. Agda has "typed holes," where you specify the goal type and the IDE

Your post is very vague, but Agda and Coq use types to help you gradually write definitions. Agda has "typed holes," where you specify the goal type and the IDE (Agda Emacs mode) will show you the relevant bindings in scope. Then, you gradually refine your definition, filling in the hole while creating new holes. Thus, Agda lets you "fill in the blank" using types as a guide. Similarity, Coq has a tactic language that builds terms, and you can see what goals there are left to fulfill and write tactic programs interactively. Agda and Coq are pure functional languages, and their type systems are a consistent logical system. They are more mathematically oriented and may not be what you want. Agda Emacs: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.htm... Coq Tactics: https://coq.inria.fr/refman/proof-engine/tactics.html https://coq.inria.fr/refman/proof-engine/tactics.html

pezo1919 7y ago
Thanks, dependent typed languages seem something to consider. Coq, Agda and Idris seem the most useful to me.
Smaug123 7y ago
Hole-based programming is something I really miss in every non-Agda language I've ever used. In particular, I code professionally in F# in such a way that it should very often be possible for the type-checker to fill holes (or at least to help me fill holes) - lots of annotations, tiny-types to encode more meaning into the types, and so on. Once you've tried agda-mode, you feel hamstrung in every other environment.
- pezo1919 7y ago
  Yes this is one main feature what I am looking for. I have just replied to another comment where I mention holes but ask a more concrete question about focusing different parts of the system when you have multiple holes. Can you please examine it? Off: may I ask how did you end up with F# and how old are you? I can't really decide the average age of programmers who do know dependent types.
  - TheAsprngHacker 7y ago
    I am a high-schooler and I understand dependent types. (I am not the person you are replying to, but I am the person who first mentioned typed holes.) In type theory, there are things called "terms" and "types." A term is something like `fun x -> x`, or `(1, 2)`, or `1 + 1`. In short, a term is basically an expression. Each term has a type. For example, `fun x -> x` might have the type `a -> a` and `(1, 2)` might have type `Nat * Nat`. If a term has a type, it "inhabits" the type. "x has type T" is written `x : T`. According to an idea called the Curry-Howard correspondence, types can encode logical statements such that terms that inhabit the type are its proofs. Therefore, by inhabiting a type, you are really proving a theorem. With dependent types, the term and type languages are the same language, so you can mix them together. In short, types are terms. Here are some types in Martin-Lof type theory: --------- () : Unit The unit type is a type with one inhabitant, (). It can be interpreted as the type of the empty tuple. In the Curry-Howard correspondence, the unit type corresponds with truth. x : A y : B -------------- (x, y) : A * B A * B, the product type of A and B, is the type of pairs. It is based on the Cartesian product operation: https://en.wikipedia.org/wiki/Cartesian_product https://en.wikipedia.org/wiki/Cartesian_product In the Curry-Howard correspondence, the product type corresponds with logical conjunction (and). By proving A and proving B, you can prove A * B (AKA A /\ B). x : Empty ---------------- elim-empty x : a The empty type is the type with no inhabitants. If you have an inhabitant of the empty type, you can eliminate it to derive anything. The empty type corresponds with falsity, and its elimination means that false implies anything. x : A -------------- Inl x : A + B x : B -------------- Inr x : A + B The sum type is the tagged union, meaning "this or that." The type A + B means that the Inl tag holds an A and the Inr tag holds a B. The sum type corresponds with logical disjunction (or). f : A -> B x : A ------------------- f(x) : B The exponential type, the type of functions, means logical implication. If you have f, a proof that A implies B, and x, a proof of A, you can prove B by doing f(x). With dependent types, the product and exponential types are generalized into the dependent sum (sigma) and the dependent product (pi) types respectively. With the dependent sum type, or sigma type `Σ (x : A) B(x)`, the second component in the type is actually a function of A (meaning that B : A -> Type). The dependent sum type generalizes the product type so that the type of the second element of the pair is actually dependent on the first element. In the Curry-Howard correspondence, the sigma type corresponds with existential quantification, "there exists" or "for some." To prove Σ (x : A) B(x), you must inhabit A (show that A exists) and B(x) (where B is a logical statement about x, the inhabitant of A). With the dependent product type, or pi type `Π (x : A) B(x)`, B is also a function of A that returns a type. The dependent product type generalizes the exponential type so that the codomain of the function, B(x), is dependent on the function's input, x. The dependent product type corresponds with universal quantification, "for all." To prove Π (x : A) B(x), you must prove B(x) for every possible x, where B(x) is a logical statement about x. Why the dependent product type generalizes the exponential type and the dependent sum type generalizes the product type seems confusing at first glance, but it really isn't: Σ for x = 1 to n, B(x) = B(1) + B(2) + ... B(n), and if B(x) is some constant C, Σ for x = 1 to n, C = n * C. The same rule applies to types, as multiplication (product) is just repeated addition (dependent sum of a constant). Π is like Σ, but for repeated multiplication instead of repeated addition. After all, exponentiation is just repeated multiplication. Another type that you should be aware of is the equality type, `x = y`. In vanilla Martin-Lof type theory, `x = y` is inhabited by `Refl` if `x` and `y` have the same normal form (reduce to the same simplest form). However, there is ongoing research in a field called Homotopy Type Theory, which redefines the equality type in various ways. Finally, types themselves form a hierarchy. With dependent types, the types themselves are first-class values, and they have their own types. However, `Type : Type` leads to Girard's paradox (similar to Russell's paradox). The solution is for each type to be in a "universe" so that `Type l : Type (l + 1)`, where `l` is the universe level. Read about Martin-Lof type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory https://en.wikipedia.org/wiki/Intuitionistic_type_theory
- jnbiche 7y ago
  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?
- lgas 7y ago
  Can you get "poor man's typed holes" in F# by using inserting unit where you would normally insert a hole and get an error message like "Couldn't match type () with type Foo"?
  - Smaug123 7y ago
    Yeah, I actually use `int` for this (because 90% of the time, if I genuinely want to use an int, I've tiny-typed it so that an int won't type-check) - but being able to see the things that are in scope of the right type at the same time would be amazing. I recognise that it would take a somewhat idiosyncratic F# coding style to make this useful, though.
    - pezo1919 7y ago
      It feels so weird. Earlier F# seemed to me a really interesting choice, but after knowing about Agda/Idris I don't feel the same anymore.
pezo1919 7y ago
Is there a way I can write you a private message with related topics? Where can I find you?

pezo1919 7y ago

Thanks, dependent typed languages seem something to consider. Coq, Agda and Idris seem the most useful to me.

Smaug123 7y ago

Hole-based programming is something I really miss in every non-Agda language I've ever used. In particular, I code professionally in F# in such a way that it should very often be possible for the type-checker to fill holes (or at least to help me fill holes) - lots of annotations, tiny-types to encode more meaning into the types, and so on. Once you've tried agda-mode, you feel hamstrung in every other environment.

pezo1919 7y ago
Yes this is one main feature what I am looking for. I have just replied to another comment where I mention holes but ask a more concrete question about focusing different parts of the system when you have multiple holes. Can you please examine it? Off: may I ask how did you end up with F# and how old are you? I can't really decide the average age of programmers who do know dependent types.
- TheAsprngHacker 7y ago
  I am a high-schooler and I understand dependent types. (I am not the person you are replying to, but I am the person who first mentioned typed holes.) In type theory, there are things called "terms" and "types." A term is something like `fun x -> x`, or `(1, 2)`, or `1 + 1`. In short, a term is basically an expression. Each term has a type. For example, `fun x -> x` might have the type `a -> a` and `(1, 2)` might have type `Nat * Nat`. If a term has a type, it "inhabits" the type. "x has type T" is written `x : T`. According to an idea called the Curry-Howard correspondence, types can encode logical statements such that terms that inhabit the type are its proofs. Therefore, by inhabiting a type, you are really proving a theorem. With dependent types, the term and type languages are the same language, so you can mix them together. In short, types are terms. Here are some types in Martin-Lof type theory: --------- () : Unit The unit type is a type with one inhabitant, (). It can be interpreted as the type of the empty tuple. In the Curry-Howard correspondence, the unit type corresponds with truth. x : A y : B -------------- (x, y) : A * B A * B, the product type of A and B, is the type of pairs. It is based on the Cartesian product operation: https://en.wikipedia.org/wiki/Cartesian_product https://en.wikipedia.org/wiki/Cartesian_product In the Curry-Howard correspondence, the product type corresponds with logical conjunction (and). By proving A and proving B, you can prove A * B (AKA A /\ B). x : Empty ---------------- elim-empty x : a The empty type is the type with no inhabitants. If you have an inhabitant of the empty type, you can eliminate it to derive anything. The empty type corresponds with falsity, and its elimination means that false implies anything. x : A -------------- Inl x : A + B x : B -------------- Inr x : A + B The sum type is the tagged union, meaning "this or that." The type A + B means that the Inl tag holds an A and the Inr tag holds a B. The sum type corresponds with logical disjunction (or). f : A -> B x : A ------------------- f(x) : B The exponential type, the type of functions, means logical implication. If you have f, a proof that A implies B, and x, a proof of A, you can prove B by doing f(x). With dependent types, the product and exponential types are generalized into the dependent sum (sigma) and the dependent product (pi) types respectively. With the dependent sum type, or sigma type `Σ (x : A) B(x)`, the second component in the type is actually a function of A (meaning that B : A -> Type). The dependent sum type generalizes the product type so that the type of the second element of the pair is actually dependent on the first element. In the Curry-Howard correspondence, the sigma type corresponds with existential quantification, "there exists" or "for some." To prove Σ (x : A) B(x), you must inhabit A (show that A exists) and B(x) (where B is a logical statement about x, the inhabitant of A). With the dependent product type, or pi type `Π (x : A) B(x)`, B is also a function of A that returns a type. The dependent product type generalizes the exponential type so that the codomain of the function, B(x), is dependent on the function's input, x. The dependent product type corresponds with universal quantification, "for all." To prove Π (x : A) B(x), you must prove B(x) for every possible x, where B(x) is a logical statement about x. Why the dependent product type generalizes the exponential type and the dependent sum type generalizes the product type seems confusing at first glance, but it really isn't: Σ for x = 1 to n, B(x) = B(1) + B(2) + ... B(n), and if B(x) is some constant C, Σ for x = 1 to n, C = n * C. The same rule applies to types, as multiplication (product) is just repeated addition (dependent sum of a constant). Π is like Σ, but for repeated multiplication instead of repeated addition. After all, exponentiation is just repeated multiplication. Another type that you should be aware of is the equality type, `x = y`. In vanilla Martin-Lof type theory, `x = y` is inhabited by `Refl` if `x` and `y` have the same normal form (reduce to the same simplest form). However, there is ongoing research in a field called Homotopy Type Theory, which redefines the equality type in various ways. Finally, types themselves form a hierarchy. With dependent types, the types themselves are first-class values, and they have their own types. However, `Type : Type` leads to Girard's paradox (similar to Russell's paradox). The solution is for each type to be in a "universe" so that `Type l : Type (l + 1)`, where `l` is the universe level. Read about Martin-Lof type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory https://en.wikipedia.org/wiki/Intuitionistic_type_theory
jnbiche 7y ago
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?
lgas 7y ago
Can you get "poor man's typed holes" in F# by using inserting unit where you would normally insert a hole and get an error message like "Couldn't match type () with type Foo"?
- Smaug123 7y ago
  Yeah, I actually use `int` for this (because 90% of the time, if I genuinely want to use an int, I've tiny-typed it so that an int won't type-check) - but being able to see the things that are in scope of the right type at the same time would be amazing. I recognise that it would take a somewhat idiosyncratic F# coding style to make this useful, though.
  - pezo1919 7y ago
    It feels so weird. Earlier F# seemed to me a really interesting choice, but after knowing about Agda/Idris I don't feel the same anymore.

pezo1919 7y ago

Is there a way I can write you a private message with related topics? Where can I find you?