Questions tagged [type-theory]
formal systems to specify properties of objects
498
questions
1
vote
1
answer
38
views
What is the difference between type inhabitant and subtyping?
I am confused with the terms inhabitant vs. subtyping.
For example,
We usually think that "john is an inhabitant of Human". This sentence is correct, because john is an individual, and an ...
- 247
4
votes
2
answers
193
views
Similarities and differences between Unit and Bottom types?
I came across this recent Reddit thread, Thoughts on Botton vs Unit Types, but I don't understand what the similarities and differences are in regards to when you are creating a programming language.
...
- 1,873
4
votes
1
answer
49
views
Covariance and Contravariance: Conflict without a Cause
Here is the last paragraph at page 441 of the paper ‘Covariance and Contravariance: Conflict without a Cause’ by Giuseppe Castagna:
How is all this translated into object-oriented type systems? ...
- 113
1
vote
0
answers
31
views
How to use debruijn indices with linear lambda calculus?
So I've been mechanizing some simple linear lambda calculus stuff.
The basic framework is
$$ \frac{}{x \colon t \vdash x\colon t} $$
$$ \frac{\Gamma \vdash e \colon t \rightarrow t' \quad \Delta \...
1
vote
1
answer
33
views
What does type theory as a theory of inductive definitions mean?
Unfortunately copy/paste doesn't work for this paper Inductive Definitions and Type Theory, but here is a snippet.
The paper begins by stating:
The first sentence of the second paragraph says type ...
- 1,873
1
vote
0
answers
16
views
How to specify a type for a SQL-like query?
What follows is a pretty complicated object (in an object-oriented, imperative, typed language), which I would like to create a type for with some sort of type annotations. I am open to how it is done,...
- 1,873
4
votes
2
answers
79
views
0
votes
0
answers
18
views
What is the general flow of the type inference algorithm in these cases where there is very little type information?
For a state of the art compiler, can they successfully do type inference on all of these cases, or are there some in which they can't? If there is a place which collects a bunch of test cases which a ...
- 1,873
0
votes
1
answer
42
views
How to think about typing inference rules when thinking about typechecking?
I am trying to build an imperative programming language with a type system that will allow for proofs. I just found kind lang, which implements all the ideas that I have been meaning to use (plus more)...
- 1,873
2
votes
0
answers
66
views
How can we derive this representation of existential types?
I know that an existential type $ \exists t. t $ can be represented using universally quantified types as $ \forall r. (\forall t. t \rightarrow r) \rightarrow r $ and I have some basic intuition for ...
4
votes
3
answers
135
views
What is the runtime/time complexity of Coq’s (Dependent) Type Inference?
I remember learning in a class that type inference is decidable but usually takes a long time (e.g. type inference in OCaml is EXPTIME).
I was wondering, since Coq allows programs/values themselves to ...
- 2,910
2
votes
0
answers
75
views
What is the runtime (time complexity) of Type Inference in Simply Typed Lambda Calculus?
I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must ...
- 2,910
4
votes
1
answer
45
views
Is sum type a disjoint or more of a multiplexer?
In Wikipedia article on "Sum Type" it is stated that sum type Curry-Howard correspondence is intuitionistic logical disjoint.
But sum type definition states that it is
a data structure used ...
- 593
2
votes
1
answer
88
views
Why does the CwF definition require a set of types under a context rather than a class of types?
In "Syntax and Semantics of Dependent Types" at the top of page 24, Martin Hoffman describes $\mathit{Ty}_{\mathcal C}(\Gamma)$ as the collection of semantic types under context $\Gamma$.
It ...
- 73
0
votes
0
answers
41
views
Is there a static type system (implemented or not) that can detect ignored parameters and re-type them to increase generality?
I came across this question while playing with the SKI combinators.
(Skip to the bottom for the question, if you don't care about the motivation.)
You can implement the combinators in Haskell as ...
- 1
0
votes
0
answers
40
views
How is the type for a sorted list defined in type theory?
I am trying to figure out what the constructor and eliminator would look like for a type representing "sorted list"?
- 593
2
votes
0
answers
50
views
Understanding least common generalization (or anti-unification) of types
I am learning how to extend a basic Hindley-Milner type system to support overloaded variables by following Geoffrey Seward Smith's dissertation.
The proposed type inference algorithm makes use of the ...
- 131
2
votes
1
answer
78
views
what precisely do linear types prevent?
"A theory of type polymorphism in programming" introduced the Hindly-Milner type system whose punchline can be summarized "well-typed terms don’t get stuck". They do this by ...
- 173
0
votes
0
answers
37
views
Axiomatic Geometry expressed with algebraic data types & functions
I've been trying to express an axiomatic geometry [1] using a typed functional language (OCaml so far).
My motivation comes from [2] and the claim "Programs correspond to logical proofs".
In ...
- 1
4
votes
0
answers
83
views
Is it possible to recover induction for nat from W-types?
W-types generalize the type of well-founded trees, i.e., possibly infinetely branching trees. I understand that inductive types may be encoded as such in dependent type theory (CIC, MLTT, etc), this ...
- 679
4
votes
2
answers
297
views
Why are Regular sets not closed under infinite unions and intersections? [duplicate]
Why are Regular sets not closed under infinite unions and intersections, with my flawled reasoning I came to a conclusion that since infinite unions can have no relationship between strings of a ...
- 221
1
vote
1
answer
70
views
What is the origin of the Bottom Type notation? Why does it look like... a bottom?
I couldn't help but notice the opening summary in Wikipedia's article on Bottom Types:
In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also ...
- 421
3
votes
0
answers
27
views
Subtype Check with Type DAG
Trying to understand how compiler/static-type-checker checks for subtyping, I run into 2 problems.
1. Reachability in DAG
Since both Python/C++ support multiple inheriatnce, the types can be ...
- 131
5
votes
1
answer
131
views
Free variables in constraint-typing derivation?
In Types and Programming Language's constraint typing rules (Figure 22-1), is it possible for any part of the typing derivation to contain free type variables that aren’t part of the fresh variables? ...
2
votes
0
answers
26
views
Do all covariant type constructors F[+A] form a functor?
Do all covariant type constructors (using scala notation) F[+A] form a functor? If so, is there a proof of that? If not, what is a counterexample?
The related Are there any type constructors which are ...
- 151
2
votes
2
answers
98
views
what are meta variables in this static analysis book's explanation about types?
At page 21 of this book: https://cs.au.dk/~amoeller/spa/spa.pdf I found this:
I started reading everything and understanding it pretty well, until this.
It's defining the possible types of a language....
- 121
1
vote
0
answers
17
views
How Should I Disambiguate Symbols for Type Placeholders and the Free Monoid Operator?
I've been writing kinds using asterisk * as a placeholder for a type. For example 𝕋 → * is the kind of all functions of time. This was fine until I needed to use ...
- 2,467
2
votes
1
answer
171
views
Which would be better for programming using Homotopy type theory Agda or Idris
I'm looking to model data inputs for an artificially intelligent system, which is affected by its internal parts and has feedback loops. I'd like to model it mathematically, using category theory or ...
- 21
1
vote
2
answers
130
views
Given an algorithm, is it possible to find all other equivalent algorithms for the same computable function in the same model
For any computable-function, there may be multiple different algorithms (possibly countably infinite). For example, sort has many different implementations/algorithms, that we know of or that we have ...
- 111
0
votes
1
answer
77
views
How do real numbers like Pi, golden ratio, etc fit into type theory
In type theory, all computable functions must terminate, however, numbers like Pi are non-terminating real numbers, hence a non-terminating function is required to compute this number, even though one ...
- 111
2
votes
1
answer
62
views
Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda
An observation when defining List in agda with --without-K enabled:
The following parameterized inductive definition is accepted:...
- 191
1
vote
1
answer
72
views
Is there a relationship between visitor pattern and DeMorgan's Law?
Visitor Pattern enables mimicking sum types with product types. Where does the "sum"-iness come from?
For example, in OCaml one could define ...
- 276
2
votes
0
answers
56
views
Do any industry programming languages use Martin-Löf style identity types?
Most programming languages have some kind of type systems but are there any programming languages widely used outside of academia (in consumer-oriented tech, finance etc.) that have intensional ...
- 21
4
votes
0
answers
64
views
What's the relationship between "semantic type soundness" and "functional correctness"?
In the Milner Award lecture "The Type Soundness Theorem That You Really Want to Prove (and now you can)" and related Sigplan blog post (with collaborators), Derek Dreyer argues that semantic ...
- 276
1
vote
0
answers
30
views
Interpreting Minimal STLC using a $\lambda 1$ Category
On page 139, example 2.4.5 of "Categorical Logic and Type Theory" by Bart Jacobs demonstrates the interpretation of the abstraction typing rule with respect to a $\lambda 1$ category. ...
- 73
2
votes
1
answer
176
views
Resources for implementing dependent type theory
I want to implement Martin Löf's intuitionistic type theory in a functional language such as Haskell, preferably also implementing a lexer/parser for the language. How should I start approaching it? ...
- 257
1
vote
1
answer
49
views
Can we somehow get functoriality from purely type-theoretic reasoning?
In this question, I asked about how to prove naturality from parametric polymorphism, using parametricity. The current answer to that question simply assumes that the functors in question satisfy the ...
- 3,464
7
votes
2
answers
207
views
Rigorous proof that parametric polymorphism implies naturality using parametricity?
This question asks for an informal explanation of why all polymorphic functions between functors are natural transformations (This is a claim made by Bartosz Milewski). One answer to that question ...
- 3,464
2
votes
1
answer
90
views
What does $\text{dom}(\Gamma)$ mean in the context of an inference rule?
In the wikipedia page on pure type systems, it gives the following inference rule:
$\frac{\Gamma \vdash A : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : A \vdash x : A }\quad \text{(start)}$
...
- 3,464
2
votes
0
answers
61
views
Resources for connections between dependent type theory and LCCC
Can someone recommend introductory articles/papers on the connections between dependent type theory and locally cartesian closed category? Many Thanks!
- 257
2
votes
1
answer
70
views
Is a system of equations derived from mutually recursive ADTs always uniquely solvable?
After looking at Can a computer determine whether a mathematical statement is true or not? for a while, I worry we may be into incompleteness/halting problem territory with this question, so an answer ...
- 615
3
votes
1
answer
97
views
Curry–Howard correspondence and functional programming "reliability"
The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness".
I recently ...
- 131
2
votes
2
answers
128
views
Does any language need to have a bottom type?
From wikipedia:
In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also called the zero or empty type, and is sometimes denoted with the up tack ...
- 123
3
votes
1
answer
366
views
What is an uninhabited type?
https://en.wikipedia.org/wiki/Type_inhabitation
The wiki article above says,
To be sound, such a system must have uninhabited types.
What is the definition an uninhabitated type? Do all programming ...
- 131
2
votes
0
answers
32
views
How to specify mutated types mathematically?
Say I have an object which I pass to a method, and the method returns that same object, just mutated.
So it goes like this:
...
- 1,873
3
votes
1
answer
152
views
Greatest fixpoint of the type of lists
I'm working through Samuel Mimram's book Program = Proof. In the first chapter, he discusses recursive types in OCaml, and inductive types. An exercise he provides on the topic has me a little bit ...
- 133
0
votes
0
answers
57
views
What is the difference between type theory and logic programming (in terms of declarative programming and specification)
How is does type theory (coq, lean, agda), and logic programming (prolog, datalog) differ from each other.
Logic programming is a way of declarative specifying an algorithm, using classical 1st order ...
- 111
8
votes
1
answer
312
views
Relationship between inductive families and type-returning functions
Dependently typed languages such as Agda support inductive families, also called indexed datatypes, which allow type parameters to vary between constructors. This can be used to define a set of ...
- 284
4
votes
1
answer
81
views
Which language is used to construct a type system?
Typically, OCaml and Scala seem to be used for designing any programming languages tool. But what features offer them an edge over other languages.
A related question, is a type system for a language ...
- 43
2
votes
1
answer
108
views
What are the most used statements in programming (ranked)?
I was wondering if there are any resources for a study/ranking of the most frequently used statements (by statements I mean assigning, invoking, instantiating etc, like in C#) in programming overall (...
- 23