Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
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 ...
user129393192's user avatar
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) ...
Guanyuming He's user avatar
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 ...
mavavilj's user avatar
  • 579
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 ...
user125234's user avatar
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 ...
Robert Wegner's user avatar
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 ...
P.A.R.T.E.I.'s user avatar
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 ...
P.A.R.T.E.I.'s user avatar
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 ...
pgmcr's user avatar
  • 36
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 $...
user125234's user avatar
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 ...
Dylech30th's user avatar
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 $\...
Raffaele Rossi's user avatar
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. ...
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
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 ...
fweth's user avatar
  • 227
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 ...
manu fava's user avatar
  • 101
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 $\...
alim's user avatar
  • 994
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
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 ...
Raffaele Rossi's user avatar
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? ...
HidekiRyuga's user avatar
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, ...
rfloc's user avatar
  • 101
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
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 ...
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
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 ...
tryst with freedom's user avatar
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 ...
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
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 ...
user32157's user avatar
  • 156
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 ...
Hank Igoe's user avatar
  • 179
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 ...
ksrk's user avatar
  • 13
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....
claydergc's user avatar
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 ...
alephalpha's user avatar
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 ...
ksrk's user avatar
  • 13
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 ...
user51462's user avatar
  • 123
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 ...
Corbin's user avatar
  • 220
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 ...
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
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 ...
A confused dove's user avatar
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 ...
chansey's user avatar
  • 285
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. ...
Lance's user avatar
  • 2,203
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
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 \...
Molly Stewart-Gallus's user avatar
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 ...
Lance's user avatar
  • 2,203
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,203
4 votes
2 answers
96 views

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

The Word type (in kind lang) looks like this: ...
Lance's user avatar
  • 2,203
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,203
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)...
Lance's user avatar
  • 2,203

1
2 3 4 5
11