# Questions tagged [type-theory]

formal systems to specify properties of objects

345 questions
Filter by
Sorted by
Tagged with
39 views

### What untyped term inhabits induction on natural numbers in CoC?

Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions. If we assumed ...
17 views

### How does this example violate Liskov substitution principle, which then causes violation of the open-closed principle?

From Agile Principles, Patterns, and Practices in C# by Robert Martin, Listing 10-1. A violation of LSP causing a violation of OCP ...
68 views

### Type theory for imperative programming languages?

The type theory that I have seen is all developed over lambda calculus, which is an inherently functional language. Nevertheless, in practice imperative languages have type systems. Are there ...
3k views

### What's the difference between a type and a kind?

I am learning the programming langauge Haskell, and I'm trying to wrap my head around what the difference between a type and a ...
140 views

### Proving that the failure of algorithm W implies that the program is not typable

How one does prove that if algorithm W failed for a given program $e$ and context $\Gamma$, then there is no substitution $S$ and type $\tau$ such that $S\Gamma \vdash e : \tau$ ? The original paper ...
25 views

### Is the expression (λx.xx)(λy.y) typeable in the following system?

We are given a simple functional language: $e ::= x | n | e_{1}e_{2}|\lambda(x:\tau).e$ with types: $\tau ::= \text{int} | \tau_{1} \rightarrow \tau_{2}| \tau_{1} \land \tau_{2}$ Is the ...
31 views

### Substituting a term for a variable in a context

At this link you can read Nicola Gambino's slides on one way to approach the formal syntax of Martin-Löf dependent type theory. (They are concise and very readable.) On slide 10, he gives a standard ...
65 views

### How is functional property guaranteed in type theory when function type is defined?

I understand that functions are not defined in type theory the same way they are defined in set theory, hence functional property is not directly defined when defining function type in type theory. ...
44 views

### Is it possible to write a fully-decidable type system for the J language?

I'm experimenting with the J array language, a dynamically-typed array language with mutable assignment, subtyping, and function overloading (just like traditional APL). It is unclear to me whether ...
33 views

### Design considerations of datatypes in early programming languages like C

Although type theory originated (e.g. already discussed by Russell in 1910s) much earlier than programming languages, I have this feeling that languages such as C considered type-checking from a very ...
30 views

### Confusion regarding algebraic specification of the queue

I was given the following question in the test where I had to write the algebraic specification and its axioms based on below-defined operations: ...
33 views

### Find typing derivation of STLC term with reference types

The problem is to find the typing derivation of a term of the call-by-value STLC extended with reference types. The evaluation and typing rules for this language is given in Types and Programming ...
52 views

### Reversing an application of sym to ua and isoToEquiv in cubical type theory

I am proving a kind of structure invariance principle for magmas in Cubical Type Theory with the Agda/Cubical library. This is done by constructing a path between two simple magmas and then ...
1k views

### Is there any use case for the bottom type as a function parameter type?

If a function has return type of ⊥ (bottom type), that means it never returns. It can for example exit or throw, both fairly ordinary situations. Presumably if a function had a parameter of type ⊥ it ...
87 views

### Can all regular tree types be expressed as $\mu$ types?

In "Types and Programming Languages", Pierce gives a translation from recursive types ($\mu$ types) to types expressed as regular trees: possibly infinite trees, but with finitely many distinct ...
33 views

25 views

### If you can have cyclic base types, or if they need to be infinite types

I am confused how to properly think about classes of classes. Basically, you can have a dog "filo" which is an instance of the dog "class". But the dog class is itself not an instanceof of "animal", ...
132 views

### Dependent type system with different computation model

There exist various Turing-equivalent models of computation, such as lambda calculus, Turing machines, or register machines. It seems that dependent type systems (like Coq, Agda, Idris, homotopy type ...
595 views

### Where are C++ templates inside of the lambda cube?

C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or ...
48 views

### What are different ways to provide a semantics to a language?

Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I ...
32 views

### Question about let syntax in type systems

I'm on the Wikipedia page for Hindley-Milner type systems, on the section about "let polymorphism": https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Let-polymorphism I'm a bit ...
45 views

### Formal name of the product of product type

What is the formal name in type theory of the operation that creates a "matrix of types" from product types (such as std::tuple in C++)? For example if we consider ...
54 views

### What is the difference between a Top type and a Unit type

Wikipedia defines a Top type: (edited for readability) The Top type [...] is the universal supertype, as all other types in any given type system are subtypes of Top However, the article goes on ...
40 views

### T&PL: Language grammar with terms

I'm autodidacting Pierce's Types and Programming Languages. On page 27 he states a definition for "terms, concretely" in constructing a language of terms, thus: For each natural number $i$, define a ...
26 views

### The underlying type theory of HOL/Isabelle

Is there a good source on the type theory of HOL/Isabelle/other HOL-based LCF-style theorem provers?
29 views

### Computational type theorists: how do you compare terms for equality here?

I am attempting to implement Simple Type Theory in the language D. How do you compare subterms to a term $R$ for the sake of computing the covering abstractors of $R$ in $M$? By reference (class ...
171 views

### Typing rule for binding groups

In "Typing Haskell in Haskell", by Mark P. Jones, is provided a sort of haskell-like specification for typing Haskell. As stated in this paper, binding groups is a area "neglected in most theoretical ...
334 views

### What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
284 views

### Drawbacks of adding type equality to 1ML

In the 1ML – Core and Modules United (F-ing First-Class Modules) paper, the author gives the following example for why module types do not form a lattice under subtyping: ...
49 views

### Mathematical resource material accompanying TAPL

I'm currently reading Types and Programming Languages by Benjamin C. Pierce and just arrived at chapter 21 Metatheory of Recursive Types. Prior to this chapter I found the book challenging but ...
90 views

I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also ...
65 views

### Is there a generally accepted name for creating types that select a subset of other types?

Tl;Dr; Given: type A = { int: foo, int: bar } type B = select foo from A What is the name of the typing relationship between A and B? What is the name of the ...
302 views

### Is the derivative of a graph related to adjacency lists?

Some of Conor McBride's works, Diff, Dissect, relate the derivative of data types to their "type of one-hole contexts". That is, if you take the derivative of the type you are left with a data type ...
25 views

### Summary of types of equivalence and equality in type theory, with notations and examples

Coming from non-computer science background, I am trying to understand the different types of equivalence and equality usually used in type theory. Ideally, I am looking for clear definitions and ...