Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more

Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
0 votes
1 answer
37 views

In what sense do universes solve the problem of not having type $\Pi_{A:\text{Type}}B(A)$?

One motivation for introducing universes, as I see it, is that without universes, we cannot construct types like $\Pi_{A:\text{Type}}B(A)$ because they would require us to have $\Gamma.\text{Type}\...
user125234's user avatar
1 vote
0 answers
37 views

Dependent Types in $\lambda P$ vs MLTT

I am trying to understand the difference between $\lambda P$ and MLT, in particular the dependent type features. What is the difference between dependent types in $\lambda P$ and dependent types in ...
IllogicalUser's user avatar
1 vote
1 answer
40 views

Adding type constructors to universes

Suppse we have a Tarski-style universe $U$, which means, in particular, that the following rules are declared: $$\frac{}{\Gamma \vdash U \text{ type}} \quad \frac{\Gamma \vdash a:U}{\Gamma \vdash \...
user125234's user avatar
2 votes
0 answers
43 views

Are there type theories for formalizing constructive metric space theory?

I suspect the type theory may not be considered fully constructive, but I am interested in hearing about any type theory that can formalize some amount of metric space theory or analysis.
IllogicalUser's user avatar
1 vote
0 answers
34 views

Analog of semantic paradoxes in type theory?

By semantic paradoxes, I mean like the Liar paradox, Curry paradox, Knower paradox, etc. In classical (logic) settings, we would need to extend the language with a predicate P (truth or is-known ...
confusedcius's user avatar
1 vote
0 answers
40 views

What is the significance of the equation $\langle \pi_1 M, \pi_2 M \rangle = M$ in $\lambda$-calculus?

When extending the simply typed $\lambda$-calculus with products, we extend $\beta$-reduction with the rules $\pi_i \langle M_1, M_2 \rangle \to_\beta M_i$, which makes sense (cf. Sørensen, Urzyczyn, ...
Danny's user avatar
  • 131
0 votes
2 answers
46 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 ...
user129393192's user avatar
2 votes
1 answer
24 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) ...
Guanyuming He's user avatar
1 vote
1 answer
117 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 ...
mavavilj's user avatar
  • 579
2 votes
2 answers
356 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 ...
Robert Wegner's user avatar
8 votes
0 answers
62 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 ...
P.A.R.T.E.I.'s user avatar
2 votes
2 answers
404 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 ...
P.A.R.T.E.I.'s user avatar
1 vote
0 answers
34 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 ...
pgmcr's user avatar
  • 36
4 votes
3 answers
674 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 ...
Dylech30th's user avatar
0 votes
0 answers
72 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 $\...
Raffaele Rossi's user avatar
5 votes
4 answers
976 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. ...
Weier's user avatar
  • 231
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 ...
Kevin Clancy's user avatar
1 vote
1 answer
77 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 ...
fweth's user avatar
  • 227
3 votes
2 answers
101 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 ...
manu fava's user avatar
  • 131
2 votes
0 answers
50 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 $\...
alim's user avatar
  • 1,014
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 ...
wildcat's user avatar
3 votes
1 answer
85 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 ...
Raffaele Rossi's user avatar
5 votes
2 answers
639 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? ...
HidekiRyuga's user avatar
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 : ...
Max Heiber's user avatar
1 vote
0 answers
60 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 ...
Jean-Baptiste's user avatar
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 ...
Rodrigo de Azevedo's user avatar
0 votes
2 answers
89 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 ...
Babu's user avatar
  • 259
0 votes
1 answer
60 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 ...
user avatar
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 ...
user avatar
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 ...
pgmcr's user avatar
  • 36
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 ...
Wasabi Kurosawa's user avatar
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 ...
Wasabi Kurosawa's user avatar
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)...
Hank Igoe's user avatar
  • 179
1 vote
0 answers
44 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 ...
user32157's user avatar
  • 156
2 votes
1 answer
66 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 ...
Hank Igoe's user avatar
  • 179
0 votes
0 answers
62 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 ...
ksrk's user avatar
  • 13
0 votes
2 answers
117 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....
claydergc's user avatar
2 votes
2 answers
205 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 ...
alephalpha's user avatar
1 vote
1 answer
63 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 ...
ksrk's user avatar
  • 13
0 votes
4 answers
259 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 ...
user51462's user avatar
  • 123
2 votes
0 answers
82 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 ...
Corbin's user avatar
  • 230
0 votes
1 answer
98 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 ...
NNNComplex's user avatar
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 ...
montokapro's user avatar
1 vote
1 answer
152 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 ...
A confused dove's user avatar
0 votes
2 answers
97 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 ...
chansey's user avatar
  • 285
3 votes
2 answers
473 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. ...
Lance's user avatar
  • 2,233
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? ...
Géry Ogam's user avatar
1 vote
0 answers
96 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 \...
Ms. Molly Stewart-Gallus's user avatar
1 vote
1 answer
66 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 ...
Lance's user avatar
  • 2,233
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,...
Lance's user avatar
  • 2,233

1
2 3 4 5
11