As in they are over hyped and offer very little use in practice.

Sure, they can offer a layer of safety on top of a program at compile time, but that safety can be implemented at run time extremely cheaply , but the sheer complexity on the language and burden on the developer is no where near justifying the nanoseconds you gain. There is a reason after decades of research, no one came up with a practical way to use them beside proving math theorems. Take the classic example of getting an element from any array. You can just do this instead:

let n: Int = 3

var m: [Int] = [1,2,3,4,5]

if n < m.count && n > 0 { print(m[n]) }

The same checks can be applied in all other "uses" of dependent types. Fuzz testing can also ensure you covered any missing cases.

Anyway, I'm not saying people are wasting their time researching and implementing them, they are interesting. But IMO they offer very little value to cost ratio.

Hi everyone. I'm currently a CS undergrad but going to grad school this year with a research focus on computational geometry. I already know Haskell and it is my go-to language so I figured the next step might be dependent types. I've been reading "Intuitionistic Type Theory" by Per Martin-Loef and it got me interested in proof assistants, specifically, Agda.

​

My question is, is it worth learning dependent types and Agda for someone who will not do any research on Programming Languages, Type Theory, or those sort of fields? Every post I've encountered mentions either HoTT or Programming Language research so I do not know if learning Agda would be worth the time in my chosen field. Any advice would be welcome :) Thanks!

I've been playing with elaboration-zoo and Checking Dependent Types with Normalization by Evaluation: A Tutorial. I tried to naively add on laziness, and I'm pretty sure I'm missing something.

type Ty = Term
type Env = [Val]


data Closure = Closure Env Term
  deriving (Show)


data Term
  = Var Int
  | Lam Term
  | App Term Term
  | LitInt Int
  | Add Term Term
  | Delay Term
  | Force Term
  deriving (Show)


data Val
  = VLam Closure
  | VVar Int
  | VApp Val Val
  | VAdd Val Val
  | VLitInt Int
  | VDelay Closure
  deriving (Show)


eval :: Env -> Term -> Val
eval env (Var x) = env !! x
eval env (App t u) =
  case (eval env t, eval env u) of
    (VLam (Closure env t), u) -> eval (u : env) t
    (t, u) -> VApp t u
eval env (Lam t) = VLam (Closure env t)
eval env (LitInt i) = VLitInt i
eval env (Add t u) =
  case (eval env t, eval env u) of
    (VLitInt a, VLitInt b) -> VLitInt (a + b)
    (t, u) -> VAdd t u
eval env (Delay t) = VDelay (Closure env t)
eval env (Force t) =
  case (eval env t) of
    VDelay (Closure env t) -> eval env t
    t -> t


quote :: Int -> Val -> Term
quote l (VVar x) = Var (l - x - 1)
quote l (VApp t u) = App (quote l t) (quote l t)
quote l (VLam (Closure env t)) = Lam (quote (1 + l) (eval (VVar l : env) t))
quote l (VLitInt i) = LitInt i
quote l (VAdd t u) = Add (quote l t) (quote l u)
quote l (VDelay (Closure env t)) = Delay t


nf :: Term -> Term
nf t = quote 0 (eval [] t)


addExample = App (Lam (Delay (Add (Var 0) (LitInt 2)))) (LitInt 2)

What do you do when quoting the delayed value? It doesn't seem right that the environment should disappear. However it also wouldn't seem right to evaluate or quote anything further because that would cause it to reduce to a normal form. If I understand correctly that the delayed value is already in a weak head normal form, and I'm thinking it is important to not continue any evaluation that isn't forced in order to be able to implement mutual recursion, and streams.

I don't know if this is a problem when using nbe for elaboration, but it certainly is a problem when pretty printing because the names of the variables that were captured in the delayed term will disappear in my implementation.

Hello, I'm reading the HoTT book and the swap function was defined as such:

https://preview.redd.it/10qoyppej5s81.png?width=974&format=png&auto=webp&s=3d9f0005ef77a1b247fc67d9b6fb7bdc85d6a30d

I've tried to prove formally that this function exists, here are the relevant rules

https://preview.redd.it/q7d25xnmj5s81.png?width=921&format=png&auto=webp&s=c3905ee93e13bc13bdc3b5b040c6130bd136d349

The problem (it seems to me) is that \b a -> g a b only makes sense when introducing both A and B into scope with their respective dependent type, however the rules only talk about introducing on dependent type one by one. What am I missing?

I've been trying to design a type theory that combines dependent types with full linear types. By "full" I mean that it has all of ⊤, ⊥, & and ⅋ from linear logic, an involutive ¬ operation on types, and instead of elimination rules it has computation rules that describe how the intro rules of a type cut against the intro rules of its dual.

In this system we can define positive equality types and negative apartness types with the following rules:

0Γ ⊦ A type
0Γ ⊦ x₀ :₀ A
0Γ ⊦ x₁ :₀ A
----
0Γ ⊦ x₀ =⁺ x₁ type


0Γ ⊦ A type
0Γ ⊦ x₀ :₀ A
0Γ ⊦ x₁ :₀ A
----
0Γ ⊦ x₀ ≠⁻ x₁ type


0Γ ⊦ A type
Γ ⊦ x :₁ A
----
Γ ⊦ refl⁺(A, x) :₁ x =⁺ x


0Γ ⊦ A type
0Γ, x₀ :₀ A, x₁ :₀ A ⊦ C type
Γ₀, x :₁ A ⊦ d :₁ ¬C[x / x₀, x / x₁]
0Γ ⊦ x₀ :₀ A
0Γ ⊦ x₁ :₀ A
Γ₁ ⊦ c :₁ C[x₀ / x₀, x₁ / x₁]
----
Γ₀₊₁ ⊦ apart⁻(A, C, d, x₀, x₁, c) :₁ x₀ ≠⁻ x₁


0Γ ⊦ A type
0Γ, x₀ :₀ A, x₁ :₀ A ⊦ C type
Γ₀, x :₁ A ⊦ d :₁ ¬C[x / x₀, x / x₁]
Γ₁ ⊦ x :₁ A
Γ₂ ⊦ c :₁ C[x / x₀, x / x₁]
----
Γ₀₊₁₊₂ ⊦ cut(refl⁺(A, x), apart⁻(A, C, d, x, x, c))
       ⇒ cut(d[x / x], c)

However an interesting fact about linear logic is that every logical concept has both a positive and a negative variant. For instance there are two "true" propositions (1 and ⊤), two "false" propositions (0 and ⊥), two "and" connectives (× and &) and two "or" connectives (+ and ⅋). This makes me think it should be possible to define negative equality types and positive apartness types. In fact, negative equality types seem straight-forward:

0Γ ⊦ A type
0Γ ⊦ x₀ :₀ A
0Γ ⊦ x₁ :₀ A
----
0Γ ⊦ x₀ =⁻ x₁ type


0Γ ⊦ A type
0Γ ⊦ x :₀ A
----
Γ ⊦ refl⁻(A, x) :₁ x =⁻ x

This is negative because it captures an arbitrary context Γ, much like the intro rule for ⊤:

----
Γ ⊦ top :₁ ⊤

What I'm wondering though is how to define the corresponding positive apartness types? I need an intro rule which is positive (which I'm taking to mean it doesn't capture a continuation context), which ensures that two values are not-equal, and which can be cut against refl⁻ to compute. I'm scratching my brain trying to come up with one though. I'm hoping someone who sees this (who maybe knows more about categorical semantics and whatnot than I do) finds this question interesting and can see an answer?

I'm toying around with writing my own dependently typed language. I followed A tutorial implementation of a dependently typed lambda calculus. So I just have a bidirectional type checker, and I added some custom modifications. For example I added polymorphic variants and rows. I also don't have any subsumption rule because I didn't need sub-typing yet, and more importantly I didn't quite understand it.

Now I want to add implicit polymorphism. For example

-- This is what the identity function would look like
id : (a : Type) -> a -> a
id _ thing = thing

-- I would like to make type variables implicit like this
id : a -> a
id thing = thing

I'm a bit confused as to what direction to go in. This is exploratory so I don't even know if I am asking the right questions.

1. I see Idris does something called elaboration. What are good sources for learning about elaboration that works with a bidirectional type checker? I got a bit lost in the Idris source code, so I want to understand it at a high level.

2. The paper Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types seems to be a solution, but in this video POPL presentation he says that figuring out how well this works with dependent types is future work.

3. It seams like it would work in most practical situations even if it ends up falling short for all situations. Is this true? Or are there other problems I might run into?

4. I seem to be missing something about how this would be implemented. I believe I would have to extend my language of types with a "FORALL" construct. Would this be going in a different direction than elaboration? Do I need both elaboration and unification, or can I just follow the paper to add onto my current typechecker.

5. Are there any other resources for adding implicit polymorphism on top of a bidirectional type checker?

Anders is HoTT theorem prover based on: classical MLTT-80 with 0, 1, 2, W types; CCHM in CHM flavour as cubical type system with hcomp/transp Kan operations; HTS strict equality on pretypes; de Rham stack modality primitives. We tend not to touch general recursive higher inductive schemes yet, instead we will try to express as much HIT as possible through W, Coequlizer and HubSpokes Disc in the style of HoTT/Coq homotopy library and Three-HIT theorem.

Written in OCaml https://github.com/groupoid/anders

I wasn't the best student in undergrad, but I've been working in software verification and validation for about 3 years now, and some of my work involves things like Coq and Idris. I enjoyed reading the HoTT book and talking online to people about PL and type theory.

Is grad school completely out of the question for me? If I do apply, are there any schools doing work in the area besides the very best?

I am interested in the design space at the intersection of region-based memory management, as present in Rust, and dependent types. In Rust lifetimes are another thing types can be parametrized by, which seems like it would translate well into a separate Sort in type theory.

I am wondering whether the additional expressiveness of dependent types would make it possible to introduce a simpler, more fundamental concept, from which references guarded by lifetimes could be derived. It would seem that the fundamental issue is that a value can become no longer usable after some other action is taken by the program, which invalidates the borrow. Is this property present in other corners of the world of type systems?

I am aware of, but not terribly familiar with ATS. It seems to me that the way they solve these issues is to require that the borrowing value is explicitly destroyed, which recovers the fractional permissions that then let you invalidate the borrow. I would like to find an approach that's not as explicit.

I find Agda's auto proof search usually gives up immediately, even if I know there must be some way of combining the definitions I have in scope to produce a term which fills the hole. Are there any dependently-typed languages that have better proof-search functionality? It doesn't even need to be clever. Just a brute-force, breadth-first search of the space of terms for something of the correct type would often be good enough if there's a solution which is simple enough, even if I have to leave it searching over night. Obviously the cleverer the better though.

So is there anything better out there? How does Coq's proof search compare for example?