Questions tagged [type-theory]
formal systems to specify properties of objects
536
questions
0
votes
1
answer
24
views
Reference types
Is a reference type (agnostic of PL) the object being pointed at, or the object doing the pointing?
I'm having a hard time wrapping my head around the concept fundamentally (of course, I have ...
2
votes
1
answer
22
views
Is limiting the input type in subclasses legitimate (does it give a stronger or the same specification)?
Note: I have read a similar post, but my problem seems different from that. Read my attempts to understand the problem for why I believe they are different.
My problem:
I know that (see this and this)
...
1
vote
1
answer
115
views
Are languages generated from a statically typed language statically typed?
Are languages generated from a statically typed language statically typed?
So say, generating Python from C++.
to generate a language from another language:
You write a transpiler in a static language ...
1
vote
0
answers
25
views
About introducing a family of types into a type theory with inference rules
Suppose I want to introduce a new family of types $B(a)$, where $a:A$ into a type theory using inference rules. First of all, my understanding is that $B:A\to U$, where $U$ is some universe. So my ...
2
votes
2
answers
339
views
Algorithm that generates verification program from solution program of NP problem
I don't know complexity class theory well so I might make some categorical errors, but I will try to ask this question anyways.
Suppose you have written a function in some programming language which ...
7
votes
0
answers
55
views
When does type inference become undecidable in typed lambda calculus?
To begin with, if I understand correctly, in a simply typed lambda calculus, typing, type checking and type inference are always decidable. In the "full-fledged" polymorphic (terms depend on ...
2
votes
2
answers
399
views
I've heard that it isn't possible to encode product types and sum types in a simply typed lambda calculus, but it seems for me that it's false
Of course, it isn't possible to construct them directly since we hasn't these type constructors, but only function constructor (arrow). But suppose there are 2 types $A$ and $B$, from which we need to ...
1
vote
0
answers
33
views
What logical system does hindley-milner correspond to, according to the curry howard correspondence?
If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a ...
0
votes
0
answers
21
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 $...
4
votes
3
answers
667
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 ...
0
votes
0
answers
57
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 $\...
5
votes
4
answers
946
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.
...
0
votes
0
answers
42
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 ...
1
vote
1
answer
74
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 ...
0
votes
1
answer
79
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 ...
1
vote
0
answers
45
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 $\...
0
votes
1
answer
66
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 ...
3
votes
1
answer
81
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 ...
5
votes
2
answers
636
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?
...
0
votes
0
answers
32
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, ...
0
votes
0
answers
22
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 : ...
1
vote
0
answers
58
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
86
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
59
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 ...
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 ...
0
votes
0
answers
37
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 ...
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
58
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
48
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)...
1
vote
0
answers
43
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 ...
2
votes
1
answer
61
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 ...
0
votes
0
answers
61
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 ...
0
votes
2
answers
116
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
191
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
...
1
vote
1
answer
62
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 ...
0
votes
4
answers
239
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 ...
2
votes
0
answers
81
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 ...
0
votes
1
answer
90
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
97
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 ...
1
vote
1
answer
150
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
95
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 ...
3
votes
2
answers
440
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.
...
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? ...
1
vote
0
answers
88
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
56
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
vote
0
answers
27
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,...
4
votes
2
answers
96
views
How does the `Word` type work in Kind Lang?
The Word type (in kind lang) looks like this:
...
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 ...
0
votes
1
answer
107
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)...