Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
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 $...
user125234's user avatar
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 ...
Dylech30th's user avatar
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 $\...
Raffaele Rossi's user avatar
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. ...
Weier's user avatar
  • 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 ...
Kevin Clancy's user avatar
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 ...
fweth's user avatar
  • 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 ...
manu fava's user avatar
  • 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 $\...
alim's user avatar
  • 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 ...
Mepep's user avatar
  • 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 ...
wildcat's user avatar
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 ...
Raffaele Rossi's user avatar
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? ...
HidekiRyuga's user avatar
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, ...
rfloc's user avatar
  • 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 : ...
Max Heiber's user avatar
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 ...
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
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 ...
tryst with freedom's user avatar
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 ...
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
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 ...
pgmcr's user avatar
  • 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 ...
Wasabi Kurosawa's user avatar
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 ...
Wasabi Kurosawa's user avatar
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)...
Hank Igoe's user avatar
  • 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 ...
user32157's user avatar
  • 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 ...
Hank Igoe's user avatar
  • 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 ...
while1fork's user avatar
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 ...
ksrk's user avatar
  • 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....
claydergc's user avatar
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 ...
alephalpha's user avatar
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 ...
ksrk's user avatar
  • 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 ...
user51462's user avatar
  • 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 ...
Corbin's user avatar
  • 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 ...
NNNComplex's user avatar
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 ...
montokapro's user avatar
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 ...
A confused dove's user avatar
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 ...
chansey's user avatar
  • 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. ...
Lance's user avatar
  • 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? ...
Géry Ogam's user avatar
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 \...
Molly Stewart-Gallus's user avatar
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 ...
Lance's user avatar
  • 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,...
Lance's user avatar
  • 2,163
4 votes
2 answers
93 views

How does the `Word` type work in Kind Lang?

The Word type (in kind lang) looks like this: ...
Lance's user avatar
  • 2,163
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 ...
Lance's user avatar
  • 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)...
Lance's user avatar
  • 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 ...
Steven Fontanella's user avatar
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 ...
Charlie Parker's user avatar
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 ...
Charlie Parker's user avatar
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 ...
al pal's user avatar
  • 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 ...
Kevin Clancy's user avatar
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"?
al pal's user avatar
  • 621

1
2 3 4 5
11