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_s...
Purescript has nice IDE integration and type holes (Haskell likely has something similar, not sure): https://qiita.com/kimagure/items/f1827c9129f3ee6ede35#type-h...
The Purescript integration seems definitely interesting!
Do you use these tools for work?
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.
It's pretty awesome.
Am I missing something?
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.
F# simply because I was looking for a functional-programming job and this was one of the first that came up. (Great personal fit, using technologies I'm not ill-disposed towards, good pay etc.)
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
x : A y : B
--------------
(x, y) : A * B
x : Empty
----------------
elim-empty x : a
x : A
--------------
Inl x : A + B
x : B
--------------
Inr x : A + B
f : A -> B x : A
-------------------
f(x) : B
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
How did study those things? Did you have any support? I have multiple programmers in my family but no one is aware of things, lol.
I learn type theory from reading on the Internet. My father is a programmer, but he mainly uses C++, so he wouldn't know type theory.
To be honest, I probably wouldn't have learned about type theory if it weren't for the Advanced Topics subculture. My first exposure to programming was with Scratch, and on the Scratch "Advanced Topics" forum (ATs), there is a subculture of people (ATers) who are more knowledgeable about programming than the average user and enjoy pushing Scratch to its limits. (I guess you could say that the ATers are hackers.) One of my friends from the ATs is interested in programming language stuff, and many people there are Lisp hackers. So, the poeple in the ATs are probably responsible for stimulating my curiosity and directing me towards functional programming and PL theory. However, I wouldn't say that I learned type theory from the ATs.
Oh yeah, I also learn type theory from people on the Fediverse (the federated social network that Mastodon uses), as there are people there who are knowleadgable about type theory.
Is there any slack channel/group you are part of? What did you find?