Questions tagged [type-theory]
formal systems to specify properties of objects
353
questions
2
votes
1answer
83 views
What does canonicity property mean in Type Theory?
The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property.
Would you please explain ...
2
votes
1answer
72 views
Difference between computation in proposition proof and definitional computation?
As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as ...
4
votes
2answers
49 views
Why values can not be replaced with their extensionally equal values in an intensional system?
Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that:
Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the ...
2
votes
1answer
47 views
Definition of extensional and propositional equality in Martin-Lof extensional type theory
Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.[4-5]) that:
A similar situation occurs in extensional Martin-Lof type theory where propositional and definitional ...
4
votes
1answer
64 views
Definitional equality of two propositions about propositional equality
Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.3) that:
It is important that definition equality is pervasive so if M and N are definitionally equal then P(M) is ...
8
votes
1answer
436 views
Representation of the concatenation at the type level
I would like to learn more about concatenative programming through the creation of a small simple language, based on the stack and following the concatenative paradigm.
Unfortunately, I haven't found ...
2
votes
0answers
34 views
Real world example of contraction and weakening
Can you provide me a real world example of contraction and weakening in the type system of a popular language like Java, Kotlin, etc.? I heard that Rust has got explicit contraction but I don´t ...
0
votes
1answer
43 views
Subtyping and subkinding, are they relevant?
I'm thinking about a type system that has some special kind of some certain types that are subtypes of the universe kind type.
Imagine the typing relation, where $...
5
votes
1answer
45 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 ...
0
votes
1answer
20 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
...
1
vote
2answers
78 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 ...
25
votes
4answers
4k 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 ...
2
votes
0answers
147 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 ...
2
votes
0answers
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 ...
1
vote
0answers
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 ...
2
votes
3answers
72 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. ...
1
vote
0answers
48 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 ...
1
vote
0answers
34 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 ...
0
votes
0answers
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:
...
0
votes
1answer
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 ...
12
votes
5answers
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 ...
6
votes
1answer
55 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 ...
6
votes
1answer
89 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 ...
2
votes
1answer
36 views
Relationship between dependent sum type and dependent product type?
Since dependent sum type ($\sum_{n\in \mathbb{N}} P(n) $) is interpreted as ($\exists n\in \mathbb{N}:P(n) $) and dependent product type ($\prod_{n\in \mathbb{N}} P(n)$) is interpreted as ($\forall n\...
3
votes
1answer
70 views
What is the relation between syntax and type theory?
Type theory and syntax are similar, in that they are inductive rules that determine whether a particular string of symbols is "correctly specified" in some sense.
There is a difference between ...
6
votes
1answer
91 views
How do we know $\neg \neg LEM$ isn't provable in MLTT?
I've been trying (fruitlessly) to prove something which I now know is not provable. Take the following definitions:
$$LEM \equiv \prod_{A : Type} \neg A \vee A$$
$$DNE \equiv \prod_{A : Type} \neg \...
1
vote
1answer
40 views
Isoecursive Types When to Fold and Unfold
I'm trying to implement recursive types into my programming language. I've implemented extensible rows and was hoping to add some recursive typing in order to get something like ...
0
votes
0answers
100 views
Definition of M-type in type theory
According to nLab, M-types are the dual of W-types. What are the introduction and elimination rules for M-types?
Edit: For example, the formation/introduction/elimination rules for W-types are:
$$\...
3
votes
1answer
68 views
How to statically type polymorphic lambdas using hindley milner style type inference
I am playing with a simple implicitly typed functional language and have implemented type checking using a Hindley Milner style system. In order to guide code generation, I want to tag each term with ...
0
votes
1answer
79 views
Is it possible to interpret some Martin-Löf types as abelian monoids in such a way that any abelian monoid can be represented as a type?
For instance, I can interpret the unit type as the trivial monoid with one element. Non-dependent pairs $A \times B$ can be interpreted as the direct sum $A ⊕ B$ when $A$ and $B$ can both be ...
3
votes
1answer
55 views
Meaning of the “why not” modality from linear type theory?
In linear type theory there is a modality written ! where !T can be read as "infinite copies of ...
5
votes
3answers
82 views
How exactly do we define parametric polymorphism?
My naive distinction between parametric polymorphism and ad-hoc polymorphism, is that:
In parametric polymorphism, the type is given as a variable: (pseudocode)
Function f: <.Type T> T $\to$...
2
votes
0answers
35 views
How can one flip a stream using corecursion
Following is the definition of codata stream:
codata Stream where
hd : Stream −> A
tl : Stream −> Stream
For simplicity I assume I have just a ...
2
votes
0answers
68 views
An Alternative History of Haskell: being lazy without class?
[The q is a play on the title of this 2007 survey of Haskell.]
tl;dr I have a couple of connected questions about Haskell's overloading mechanisms. I'll ask first then explain why. I'm looking at the ...
5
votes
2answers
79 views
Identity types and universes
Let us consider Martin-Löf type theory with a cumulative hierarchy of universes
$$
\mathcal{U}_0\colon\mathcal{U}_1\colon\ldots
$$
If $A, B\colon \mathcal{U}_i$, we can form an identity type $A=_{\...
0
votes
0answers
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", ...
2
votes
1answer
135 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 ...
5
votes
1answer
599 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 ...
3
votes
1answer
49 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 ...
2
votes
0answers
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 ...
3
votes
1answer
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 ...
2
votes
1answer
62 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 ...
1
vote
0answers
27 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?
0
votes
0answers
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 ...
3
votes
1answer
291 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:
...
4
votes
1answer
172 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 ...
0
votes
0answers
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 ...
3
votes
1answer
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 ...
1
vote
0answers
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 ...
4
votes
1answer
95 views
Roadmap to formal verification
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 ...
