Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
1 vote
1 answer
28 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
0 answers
13 views

Co-refinement or PER-refinement types

I just learned about LiquidHaskell, which is Haskell with refinement types. As pointed out by drcicero, the type former that sets apart a refinement type system from a simple type system is the type ...
  • 101
0 votes
4 answers
113 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 ...
  • 101
2 votes
0 answers
53 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 ...
  • 211
0 votes
1 answer
46 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
52 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
123 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 ...
1 vote
1 answer
50 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 ...
  • 247
3 votes
2 answers
249 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. ...
  • 1,931
4 votes
1 answer
58 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
37 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
42 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,931
1 vote
0 answers
19 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,...
  • 1,931
4 votes
2 answers
86 views

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

The Word type (in kind lang) looks like this: ...
  • 1,931
0 votes
0 answers
20 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 ...
  • 1,931
0 votes
1 answer
47 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)...
  • 1,931
2 votes
0 answers
69 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
161 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 ...
2 votes
0 answers
100 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 ...
4 votes
1 answer
48 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 ...
  • 593
2 votes
1 answer
93 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 ...
0 votes
0 answers
43 views

Is there a static type system (implemented or not) that can detect ignored parameters and re-type them to increase generality?

I came across this question while playing with the SKI combinators. (Skip to the bottom for the question, if you don't care about the motivation.) You can implement the combinators in Haskell as ...
  • 1
0 votes
0 answers
42 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"?
  • 593
2 votes
0 answers
54 views

Understanding least common generalization (or anti-unification) of types

I am learning how to extend a basic Hindley-Milner type system to support overloaded variables by following Geoffrey Seward Smith's dissertation. The proposed type inference algorithm makes use of the ...
  • 131
2 votes
1 answer
80 views

what precisely do linear types prevent?

"A theory of type polymorphism in programming" introduced the Hindly-Milner type system whose punchline can be summarized "well-typed terms don’t get stuck". They do this by ...
4 votes
0 answers
87 views

Is it possible to recover induction for nat from W-types?

W-types generalize the type of well-founded trees, i.e., possibly infinetely branching trees. I understand that inductive types may be encoded as such in dependent type theory (CIC, MLTT, etc), this ...
4 votes
2 answers
317 views

Why are Regular sets not closed under infinite unions and intersections? [duplicate]

Why are Regular sets not closed under infinite unions and intersections, with my flawled reasoning I came to a conclusion that since infinite unions can have no relationship between strings of a ...
1 vote
1 answer
73 views

What is the origin of the Bottom Type notation? Why does it look like... a bottom?

I couldn't help but notice the opening summary in Wikipedia's article on Bottom Types: In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also ...
  • 421
3 votes
0 answers
27 views

Subtype Check with Type DAG

Trying to understand how compiler/static-type-checker checks for subtyping, I run into 2 problems. 1. Reachability in DAG Since both Python/C++ support multiple inheriatnce, the types can be ...
  • 131
5 votes
1 answer
140 views

Free variables in constraint-typing derivation?

In Types and Programming Language's constraint typing rules (Figure 22-1), is it possible for any part of the typing derivation to contain free type variables that aren’t part of the fresh variables? ...
2 votes
0 answers
26 views

Do all covariant type constructors F[+A] form a functor?

Do all covariant type constructors (using scala notation) F[+A] form a functor? If so, is there a proof of that? If not, what is a counterexample? The related Are there any type constructors which are ...
  • 151
2 votes
2 answers
118 views

what are meta variables in this static analysis book's explanation about types?

At page 21 of this book: https://cs.au.dk/~amoeller/spa/spa.pdf I found this: I started reading everything and understanding it pretty well, until this. It's defining the possible types of a language....
  • 121
1 vote
0 answers
17 views

How Should I Disambiguate Symbols for Type Placeholders and the Free Monoid Operator?

I've been writing kinds using asterisk * as a placeholder for a type. For example 𝕋 → * is the kind of all functions of time. This was fine until I needed to use ...
  • 2,495
2 votes
1 answer
224 views

Which would be better for programming using Homotopy type theory Agda or Idris

I'm looking to model data inputs for an artificially intelligent system, which is affected by its internal parts and has feedback loops. I'd like to model it mathematically, using category theory or ...
  • 21
1 vote
2 answers
139 views

Given an algorithm, is it possible to find all other equivalent algorithms for the same computable function in the same model

For any computable-function, there may be multiple different algorithms (possibly countably infinite). For example, sort has many different implementations/algorithms, that we know of or that we have ...
  • 111
0 votes
1 answer
78 views

How do real numbers like Pi, golden ratio, etc fit into type theory

In type theory, all computable functions must terminate, however, numbers like Pi are non-terminating real numbers, hence a non-terminating function is required to compute this number, even though one ...
  • 111
2 votes
1 answer
67 views

Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda

An observation when defining List in agda with --without-K enabled: The following parameterized inductive definition is accepted:...
  • 191
1 vote
1 answer
72 views

Is there a relationship between visitor pattern and DeMorgan's Law?

Visitor Pattern enables mimicking sum types with product types. Where does the "sum"-iness come from? For example, in OCaml one could define ...
2 votes
0 answers
62 views

Do any industry programming languages use Martin-Löf style identity types?

Most programming languages have some kind of type systems but are there any programming languages widely used outside of academia (in consumer-oriented tech, finance etc.) that have intensional ...
  • 21
4 votes
0 answers
75 views

What's the relationship between "semantic type soundness" and "functional correctness"?

In the Milner Award lecture "The Type Soundness Theorem That You Really Want to Prove (and now you can)" and related Sigplan blog post (with collaborators), Derek Dreyer argues that semantic ...
1 vote
0 answers
30 views

Interpreting Minimal STLC using a $\lambda 1$ Category

On page 139, example 2.4.5 of "Categorical Logic and Type Theory" by Bart Jacobs demonstrates the interpretation of the abstraction typing rule with respect to a $\lambda 1$ category. ...
2 votes
1 answer
241 views

Resources for implementing dependent type theory

I want to implement Martin Löf's intuitionistic type theory in a functional language such as Haskell, preferably also implementing a lexer/parser for the language. How should I start approaching it? ...
1 vote
1 answer
53 views

Can we somehow get functoriality from purely type-theoretic reasoning?

In this question, I asked about how to prove naturality from parametric polymorphism, using parametricity. The current answer to that question simply assumes that the functors in question satisfy the ...
  • 3,382
8 votes
3 answers
238 views

Rigorous proof that parametric polymorphism implies naturality using parametricity?

This question asks for an informal explanation of why all polymorphic functions between functors are natural transformations (This is a claim made by Bartosz Milewski). One answer to that question ...
  • 3,382
2 votes
1 answer
115 views

What does $\text{dom}(\Gamma)$ mean in the context of an inference rule?

In the wikipedia page on pure type systems, it gives the following inference rule: $\frac{\Gamma \vdash A : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : A \vdash x : A }\quad \text{(start)}$ ...
  • 3,382
2 votes
0 answers
62 views

Resources for connections between dependent type theory and LCCC

Can someone recommend introductory articles/papers on the connections between dependent type theory and locally cartesian closed category? Many Thanks!
2 votes
1 answer
71 views

Is a system of equations derived from mutually recursive ADTs always uniquely solvable?

After looking at Can a computer determine whether a mathematical statement is true or not? for a while, I worry we may be into incompleteness/halting problem territory with this question, so an answer ...
3 votes
1 answer
100 views

Curry–Howard correspondence and functional programming "reliability"

The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness". I recently ...
  • 131
2 votes
2 answers
133 views

Does any language need to have a bottom type?

From wikipedia: In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also called the zero or empty type, and is sometimes denoted with the up tack ...
3 votes
1 answer
488 views

What is an uninhabited type?

https://en.wikipedia.org/wiki/Type_inhabitation The wiki article above says, To be sound, such a system must have uninhabited types. What is the definition an uninhabitated type? Do all programming ...
  • 131

1
2 3 4 5
11