New answers tagged type-theory
1
As mentioned by Andrej, this is an instance of transporting along an equivalence of families and display maps. In this specific case, we have an equivalence of graphs and relations.
open import Function
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Level renaming (zero to lzero; suc to lsuc)
-- type of relations on a ...
4
OCaml and Scala are popular choices for types systems, but they are by no means the only languages you can write a compiler, interpreter, typechecker, or type system in.
Type-checking involves traversing syntax trees representing terms and types. Languages with some form of algebraic data type make this easy, since these traversals can be defined using ...
2
I think the best way to understand why homotopy type theory related stuff is interesting from a computer science perspective is that is a more satisfying account of extensional equality than any prior version. Lots of attempts have been made previously to add extensionality features to type theory that have been missing relative to e.g. set theory, but they ...
5
$\newcommand{\fix}{\mathsf{fix}}$
$\newcommand{\fold}{\mathsf{fold}}$
$\newcommand{\map}{\mathsf{map}}$
Here is, I believe, how one would use parametricity to prove your last lemma. I'm going to rework some stuff slightly for my own understanding. We have: $$C = ∀ r. (F r → r) → r$$ with $F$ functorial. We have: $$\fix : F C → C$$ corresponding to your ...
2
I don't know about statement types, but there's been a lot of research over the decades about CPU instruction frequency and how it impacts ISA design, IR design, and VM design... but it's all for languages like C. See, for example, loads/stores/branch frequencies for the SPEC2017 benchmarks.
If your language is C-like, there are basically only two reasons to ...
Top 50 recent answers are included
