Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
1 vote
1 answer
38 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 ...
user avatar
  • 247
4 votes
2 answers
193 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. ...
user avatar
  • 1,873
4 votes
1 answer
49 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? ...
user avatar
  • 113
1 vote
0 answers
31 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 \...
user avatar
1 vote
1 answer
33 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 ...
user avatar
  • 1,873
1 vote
0 answers
16 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,...
user avatar
  • 1,873
4 votes
2 answers
79 views

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

The Word type (in kind lang) looks like this: ...
user avatar
  • 1,873
0 votes
0 answers
18 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 ...
user avatar
  • 1,873
0 votes
1 answer
42 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)...
user avatar
  • 1,873
2 votes
0 answers
66 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 ...
user avatar
4 votes
3 answers
135 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 ...
user avatar
2 votes
0 answers
75 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 ...
user avatar
4 votes
1 answer
45 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 ...
user avatar
  • 593
2 votes
1 answer
88 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 ...
user avatar
0 votes
0 answers
41 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 ...
user avatar
  • 1
0 votes
0 answers
40 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"?
user avatar
  • 593
2 votes
0 answers
50 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 ...
user avatar
  • 131
2 votes
1 answer
78 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 ...
user avatar
0 votes
0 answers
37 views

Axiomatic Geometry expressed with algebraic data types & functions

I've been trying to express an axiomatic geometry [1] using a typed functional language (OCaml so far). My motivation comes from [2] and the claim "Programs correspond to logical proofs". In ...
user avatar
  • 1
4 votes
0 answers
83 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 ...
user avatar
4 votes
2 answers
297 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 ...
user avatar
1 vote
1 answer
70 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 ...
user avatar
  • 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 ...
user avatar
  • 131
5 votes
1 answer
131 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? ...
user avatar
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 ...
user avatar
  • 151
2 votes
2 answers
98 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....
user avatar
  • 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 ...
user avatar
  • 2,467
2 votes
1 answer
171 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 ...
user avatar
  • 21
1 vote
2 answers
130 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 ...
user avatar
  • 111
0 votes
1 answer
77 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 ...
user avatar
  • 111
2 votes
1 answer
62 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:...
user avatar
  • 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 ...
user avatar
2 votes
0 answers
56 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 ...
user avatar
  • 21
4 votes
0 answers
64 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 ...
user avatar
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. ...
user avatar
2 votes
1 answer
176 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? ...
user avatar
1 vote
1 answer
49 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 ...
user avatar
  • 3,464
7 votes
2 answers
207 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 ...
user avatar
  • 3,464
2 votes
1 answer
90 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)}$ ...
user avatar
  • 3,464
2 votes
0 answers
61 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!
user avatar
2 votes
1 answer
70 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 ...
user avatar
3 votes
1 answer
97 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 ...
user avatar
  • 131
2 votes
2 answers
128 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 ...
user avatar
3 votes
1 answer
366 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 ...
user avatar
  • 131
2 votes
0 answers
32 views

How to specify mutated types mathematically?

Say I have an object which I pass to a method, and the method returns that same object, just mutated. So it goes like this: ...
user avatar
  • 1,873
3 votes
1 answer
152 views

Greatest fixpoint of the type of lists

I'm working through Samuel Mimram's book Program = Proof. In the first chapter, he discusses recursive types in OCaml, and inductive types. An exercise he provides on the topic has me a little bit ...
user avatar
  • 133
0 votes
0 answers
57 views

What is the difference between type theory and logic programming (in terms of declarative programming and specification)

How is does type theory (coq, lean, agda), and logic programming (prolog, datalog) differ from each other. Logic programming is a way of declarative specifying an algorithm, using classical 1st order ...
user avatar
  • 111
8 votes
1 answer
312 views

Relationship between inductive families and type-returning functions

Dependently typed languages such as Agda support inductive families, also called indexed datatypes, which allow type parameters to vary between constructors. This can be used to define a set of ...
user avatar
4 votes
1 answer
81 views

Which language is used to construct a type system?

Typically, OCaml and Scala seem to be used for designing any programming languages tool. But what features offer them an edge over other languages. A related question, is a type system for a language ...
user avatar
2 votes
1 answer
108 views

What are the most used statements in programming (ranked)?

I was wondering if there are any resources for a study/ranking of the most frequently used statements (by statements I mean assigning, invoking, instantiating etc, like in C#) in programming overall (...
user avatar
  • 23

1
2 3 4 5
10