Questions tagged [type-theory]
formal systems to specify properties of objects
530
questions
0
votes
0
answers
19
views
Would this subtyping relation contradict disjointness?
This is a basic question, but suppose I have two disjoint universes $\mathcal A $ and $\mathcal B$, and some fixed types $A:\mathcal A, B:\mathcal B$. Would it contradict anything if I postulate that $...
- 101
4
votes
3
answers
636
views
What is practically preventing us from applying set-theoretic types in engineering?
I know the title is sort of misleading because we do have set-theoretic types in several languages:) From a theoretic view, set-theoretic types such as intersection, union, and negation may bring some ...
- 43
0
votes
0
answers
47
views
Proof that the Omega combinator cannot be typed in System F
I was reading Type Theory and Formal Proof by Nederpelt and Geuvers and in Chapter 3 about $\lambda2$ at page 81 they show how the self-applicator $\lambda x . xx$ can be typed by observing that $\...
- 165
5
votes
4
answers
880
views
Curry-Howard isomorphism and non-constructive logic
My understanding of the Curry–Howard correspondence is that it shows an isomorphism between constructive logic (also called intuitionistic logic) and computer programs in appropriate typed languages.
...
- 181
0
votes
0
answers
40
views
Categorical interpretation of beta-reduction for mu abstractions in lambda-mu calculus
I've been reading the Peter Selinger's article "Control Categories and Duality: On the Categorical Semantics of the Lambda-Mu Calculus". I'm wondering about the categorical interpretation of ...
- 173
1
vote
1
answer
60
views
`transp` In Agda
I'm still a bit confused about the transp operator in Agda:
transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1
Is found ...
- 227
0
votes
1
answer
73
views
Relation between Curry-Howard isomorphism and Kripke semantics for intuitionistic logic
Intuitionistic logic(s) are usually defined in a purely synthetic way, with their own deduction rules different from classical logic, but they also have semantic interpretations.
One of them, more ...
- 101
1
vote
0
answers
42
views
Is this a correct way of using structural induction to prove type uniqueness?
I was reading the book "Types and Programming Languages" by Benjamin C. Pierce, paying attention to proofs so I could learn proof techniques.
In the parts discussing the simply typed $\...
- 984
1
vote
0
answers
38
views
Difference between structural and derivation induction
I am currently reading the book "Programming Languages and Types" by Benjamin C. Pierce. The myriad usage of many different kinds of inductive proofs has started to confuse me a bit.
For my ...
- 11
0
votes
1
answer
59
views
Is it possible for a language to have mixed evaluation strategies?
As far as I am aware, most functional programming languages today use a call-by-value eager evaluation strategy with some exceptions like Haskell. I am curious if it is possible for a language to have ...
- 1
3
votes
1
answer
75
views
Is shadowing of the type variable allowed in System F second order abstraction?
I'm reading Type Theory and Formal Proof by Nederpelt and Geuvers. Chapter 3 is about $\lambda 2$ and $\Pi$-Types (aka System F, I think?) and the derivation rule for 2nd order abstraction seems to ...
- 165
5
votes
2
answers
634
views
Structural equivalence of self-referential structures
Given two types, T1 and T2, how does structural equivalence work when they're self-referential? Further, how do we go about proving it?
...
- 59
0
votes
0
answers
26
views
Introduction to Calculus of Inductive Constructions
Which books/notes teach Calculus of Inductive Constructions (CIC) without using a specific programming languages like Coq or Lean? I would like a reference that also doesn’t assume (naive) set theory, ...
- 101
0
votes
0
answers
21
views
What are the similarities and differences between dependent function application and ML functor application?
Advanced Topics in Types and Programming Languages gives this rule section 2.2 gives this rule for dependent function application:
$$\frac{\Gamma \vdash t_1 : (\Pi x : S.T) \quad \Gamma \vdash t_2 : ...
- 346
1
vote
0
answers
57
views
How do you deal with Skolem functions which escape their scope in elimination rules?
If you have an elimination rule for tuples which introduce the left and right pair into the type checking context, what do you do if the type of one of the elements is quantified and has been ...
1
vote
0
answers
37
views
What is the type of a type signature?
For example, using GHCi,
ghci> f x = x + 1
ghci> :t f
f :: Num a => a -> a
What is the type of the type signature ...
0
votes
2
answers
82
views
Why would we want to define new types in a functional programming language?
I am a total noob to programming, and one of the basic ideas in Haskell is how one can define new types using some things called constructors. I haven't quite understood it fully, but why would one ...
0
votes
1
answer
52
views
How to find a term that proves a given proposition?
I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of ...
user157472
1
vote
1
answer
44
views
Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$
Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are ...
user157472
0
votes
0
answers
35
views
Ambiguous type of "triangle" operator for sum types
In Meijer, Fokkinga and Patersons "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" the ∇ operator for sum types is introduced which removes the tags from its ...
- 26
1
vote
1
answer
52
views
How is the direct product of the functions (A -> B) * (C -> D) equivalent to the function (A * C) -> (B * D)? Is there an error here?
In the simply typed lambda calculus we have type algebra - types can be added, multiplied and exponentiated, where addition corresponds to the sum type, multiplication to the product type, and ...
1
vote
1
answer
53
views
On the logical and categorical interpretation of lambda calculi and type systems
There is a well-known Curry-Howard-Lambek correspondence between certain type systems, proof calculi and categories.
Some variants of Barendregt's pure type systems have the property of strong ...
0
votes
2
answers
46
views
Types and programming languages: strange term construction?
Pierce's Types and Programming Languages has the following definition of terms:
$$S_0=\emptyset$$
$$S_{i+1} = \{true,false,0\} \cup \{succ(t), pred(t),iszero(t)|t \in S_i\} \cup\{if(t_1)then (t_2)...
- 179
1
vote
0
answers
41
views
What types can be written in Kind but not Lean?
The Kind programming language has a sufficiently powerful type system to support proving theorems like in Lean, Coq, Idris, or Agda. I've seen it said that Kind has an even more powerful type system ...
- 156
2
votes
1
answer
53
views
Top type in JavaScript?
I am wondering, what is the top type, $\top$, in JavaScript? The diagrams at MDN make it look as if 'null' is a top type, but wikipedia's entry for top type indicate that it is Object in JS, which ...
- 179
1
vote
0
answers
93
views
Can the Calculus of Constructions (without inductives) be used to axiomatize mathematics?
I'm aware that proof assistants like Coq and Agda are based on CIC rather than CoC because there is e.g. no inductive natural number type in CoC. Therefore, for example the proof that addition is ...
- 329
0
votes
0
answers
55
views
Is type inference for arbitrary-rank types decidable when supplied type signatures?
I found following statements in 6.4.16. Arbitrary-rank polymorphism of ghc document.
GHC uses an algorithm proposed by Odersky and Laufer (“Putting type annotations to work”, POPL‘96) to get a ...
- 13
0
votes
2
answers
108
views
How to represent a point cloud in the pseudocode of an algorithm?
I am writing a scientific paper in which I describe some algorithms (using pseudocode) that have point clouds as inputs. In these algorithms, I need a mathematical structure to represent a point cloud....
2
votes
2
answers
172
views
The second Functor law is redundant, but I don't understand the proof
When we defining a Functor instance in Haskell, it should satisfy the following two laws:
fmap id = id
...
- 123
1
vote
1
answer
59
views
How does GHC insert type abstraction/application under the RankNTypes extension
I'm developing a functional programming language that offers Rank-n polymorphism. Like Haskell I don't want types to appear at the term level, but I have no idea to insert type abstraction and type ...
- 13
0
votes
4
answers
193
views
Are integers an abstract data type?
I'm trying to understand whether integers are an abstract data type.
The Wikipedia article starts out by saying that integers are not an ADT:
In practice, many common data types are not ADTs, as the ...
- 123
2
votes
0
answers
78
views
What are strong examples of programming languages whose type systems don't embed into their native type theory?
Given a typical popular programming language, its native type theory is a dependent type theory which describes invariants, preconditions, predicates, and other generalizations of typical type-system ...
- 220
0
votes
1
answer
77
views
Relationship between cartesian product and dependent product type
Introduction:
Hi, I'm quite new to types so apologies in advance for the basic question and for any abuse of terminology. I believe I have a critical misunderstanding of dependent product types (and ...
2
votes
1
answer
86
views
Is the root function computationally equivalent to function application?
If a function type is representable by exponentiation, does it follow that function application is represented by the right inverse, roots? It would seem that roots consume a function's input to ...
- 21
1
vote
1
answer
146
views
Proving transitivity in an intuitionistic type theory without the K rule
In Agda, if I disable axiom $\mathbb{K}$ I'm not able to prove
$$
\forall\{A : \textbf{Set}\}\{a\ b : A\}\{p\ q : a \equiv b\} \to p \equiv q,
$$
which I guess is normal since the system does not ...
0
votes
2
answers
93
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 ...
- 275
3
votes
2
answers
384
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.
...
- 2,163
4
votes
1
answer
67
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
84
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
53
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 ...
- 2,163
1
vote
0
answers
24
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,...
- 2,163
4
votes
2
answers
93
views
0
votes
0
answers
27
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 ...
- 2,163
0
votes
1
answer
87
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)...
- 2,163
2
votes
0
answers
86
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
306
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 ...
- 3,000
3
votes
0
answers
241
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 ...
- 3,000
4
votes
1
answer
55
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 ...
- 621
2
votes
1
answer
110
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 ...
- 173
0
votes
0
answers
46
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"?
- 621