Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
0
votes
0answers
37 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
1answer
51 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
2answers
114 views

How do you have a type typed “Type” when implementing a programming language?

I am working on the base of a language model, and am wondering how to represent the base type, which is a type Type. I have heard of an "infinite chain of ...
5
votes
2answers
752 views

Question on the “Tutorial implementation of dependently typed lambda calculus”

I have a slight technical struggle with this marvelous tutorial. On page 5 the tutorial talks about typing rules for Simply Typed Lambdas and presents following judgement as derivable via rules on ...
6
votes
1answer
762 views

Why product type is a dependent SUM?

It might just be a stupid question but I simply see no obvious reason why dependent sum type is a generalized form of product type. Concretely, the sigma type $\Sigma(x:S)T$ degenerates to a product ...
1
vote
1answer
113 views

Creating a large tuple from smaller tuples via a monad or applicative

Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term $\lambda x_{\beta}. \;(x, \, ...
2
votes
1answer
55 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 ...
2
votes
2answers
94 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
1answer
52 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 ...
0
votes
0answers
21 views

Generalised letrec semantics for mutual recursion

I'm new to system types and I was wondering how mutual recursion is defined through generalized e::= ..|let rec x1=e1 ,...., xn=en in e .What has to be added in the "simple" let rec ...
4
votes
0answers
75 views

Understanding a paper on polynomial recursion in all finite types

So I wasn't sure weather or not this counted as "research level" or not but I figured it wasn't so I decided to post it here. There is a paper by S. Bellantoni et al. called "Higher ...
2
votes
0answers
25 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: ...
2
votes
1answer
51 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 ...
0
votes
0answers
42 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 ...
5
votes
1answer
273 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 ...
2
votes
1answer
65 views
3
votes
1answer
67 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 ...
4
votes
2answers
136 views

What are the implications of Homotopy Type Theory?

I've recently come across the topic of homotopy type theory and I'm interested to learn more. I have a very limited background in type theory. Can anyone tell me, in functional programming terms or ...
3
votes
1answer
107 views

How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?

The well-known Church encoding of natural numbers can be generalized to use an arbitrary (covariant) functor F. The result is the type, call it ...
2
votes
1answer
62 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 (...
0
votes
0answers
28 views

Is the borrow checker mechanism in Rust based on quantitative types?

I was trying to understand if the borrow checking mechanism for references is actually a quantitaive type in disguise because it does look very similar. In case these are just similar but unrelated ...
2
votes
4answers
433 views

Is there such thing as “sequential types”?

I am wondering how you could possibly define the implementation of an imperative function as a type. Is it possible? Currently I only see the input parameters and output result used in the definition ...
1
vote
2answers
78 views

Interpreting a proof of $2^\mathbb{N}$ being uncountable

Suppose I have the following proof: ...
0
votes
0answers
87 views

Can we think of a non-symmetric product type in Haskell?

Meta note: I asked this question here a while ago. It got an answer: type a /\!! b = (a, ((b -> Void) -> Void)) Unfortunately, I do not reckon it to be ...
1
vote
1answer
97 views

What's the difference between Row Polymorphism and Structural Typing?

The definitions I've stumbled across seem to indicate they express the same idea. That's that the relationship between record types is determined by their fields (or properties) rather than their ...
1
vote
1answer
38 views

Example of Dependent Types?

Say you have 3 objects, a global MemoryStore, which has an array of MemorySlabCache objects, and each ...
0
votes
0answers
65 views

Consistency of a set of bidirectional typing rules

Main Is there any way to algorithmically check the consistency of a set of bidirectional typing rules, e.g. the absence of cycles and the uniqueness of the derivation tree? This problem is naturally ...
2
votes
1answer
63 views

Does canonicity imply weak normalization?

Context: type theory. My understanding of: WN: every term can rewrite to NF. Canonicity: every term rewrites into canonical form. Then it leads to an intuition where if canonicity holds, then we get ...
3
votes
0answers
50 views

Semantics of “write-once” variables for complex data structures

Question My use case for what is described below is not a language or compiler implementation, but finding a reasonable semantics for this feature in a an abstract calculus. Ideally, you give me a ...
4
votes
1answer
364 views

Why do we need a separate notation for П-types?

Main I am confused about the motivation behind the need for a separate notation for П-types, that you can find in type systems from λ2 on. The answer usually goes like so - think about how one can ...
1
vote
0answers
91 views

How do type classes make ad-hoc polymorphism less ad hoc?

The title of the paper that introduced type classes is "How to make ad-hoc polymorphism less ad hoc". It seems the type classes approach is being compared to how OOP does ad-hoc polymorphism....
3
votes
0answers
91 views

(Co)-monads and terminating implementations

The bounty above should read 'I would like to know whether the example I discuss is a com-monad and why (why not).' Suppose we set $\mathbb{M} \alpha := r \to \alpha$, where $r$ is some fixed type, ...
3
votes
1answer
255 views

The meaning and relevance of the locution ''no terminating implementation'' in type theory

In the context of a discussion of Haskell https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, I was told that There is no terminating ...
2
votes
0answers
44 views

Difference between the logic and the type system of a proof assistant?

In Comparing Mathematical Provers (section 4.1), Wiedijk classifies logics and type systems of different proof assistants? I do not see what he means by type system of the assistant. He only says: A ...
1
vote
2answers
82 views

How to express a type that represents an associative array whose keys determine the type of the value?

I'm fairly new to type systems and theory, so I would appreciate some guidance in a problem that sparked my interest. I would like to understand what type system features are required so a compiler ...
2
votes
0answers
51 views

Inhabitation of STLC is in PSPACE

Urzyczyn: Inhabitation in Typed Lambda-Calculi (A syntactic approach) gives a proof that STLC inhabitation problem is in PSPACE (section 2, lemma 1). I don't understand certain aspects of the proof: ...
1
vote
1answer
104 views

Is it possible to interpret some Martin-Löf types as abelian monoids in such a way that any abelian monoid can be represented as a type?

For instance, I can interpret the unit type as the trivial monoid with one element. Non-dependent pairs $A \times B$ can be interpreted as the direct sum $A ⊕ B$ when $A$ and $B$ can both be ...
1
vote
1answer
48 views

Terms for different models of sum types

There seem to be at least a couple different possible ways of modeling sum types in a type system, but I haven't been able to find consistent terms for referring to them: A sum type is formed from a ...
6
votes
2answers
346 views

What kinds of programming pitfalls modern languages are able to find?

I often see claims that modern functional strictly-typed languages are 'safer' than others. These statement mostly linked with type systems and their ability to explicitly express the following ...
3
votes
1answer
58 views

The underlying type theory of HOL/Isabelle

Is there a good source on the type theory of HOL/Isabelle/other HOL-based LCF-style theorem provers?
24
votes
1answer
2k views

What are the strongest known type systems for which inference is decidable?

It's well known that Hindley–Milner type inference (the simply-typed $\lambda$-calculus with polymorphism) has decidable type inference: you can reconstruct principle types for any programs without ...
4
votes
2answers
102 views

Meaning of the “why not” modality from linear type theory?

In linear type theory there is a modality written ! where !T can be read as "infinite copies of ...
1
vote
0answers
22 views

Does Quantitative Type Theory make the Prop universe obsolete?

Coq (and other type theories such as Setoid Type Theory) have a Prop universe for propositions. As far as I understand this universe is needed to be sure that the propositions can be erased. In ...
0
votes
0answers
32 views

Is Observational Equality better than intensional equality?

The Observational Equality from Epigram 2 seems to be intensional equality (like Coq and Agda have), but it also supports function extensionality. In that sense it seems that Observational Equality is ...
1
vote
0answers
24 views

Is there a most general fixpoint?

We can write inductive types in terms of a fixpoint type: ...
66
votes
4answers
12k views

Dependent types vs refinement types

Could somebody explain the difference between dependent types and refinement types? As I understand it, a refinement type contains all values of a type fulfilling a predicate. Is there a feature of ...
2
votes
0answers
86 views

Summary of types of equivalence and equality in type theory, with notations and examples

Coming from non-computer science background, I am trying to understand the different types of equivalence and equality usually used in type theory. Ideally, I am looking for clear definitions and ...
2
votes
1answer
93 views

Difference between assignment, binding, and substitution?

I am trying to understand the difference of assignment, binding, and substitution. I know the three things are related, but to me it's not exactly clear what word refers to what. Example, illustration,...
1
vote
1answer
53 views

Substitution lemma for types

TAPL (page 549) proposes the following lemma in order to prove soundness of System F type system: Substitution lemma for types: $E, X, \Delta \vdash t: T \implies E, [X \mapsto S] \Delta \vdash [X \...
1
vote
0answers
41 views

The abstract interpretation corresponding to the pure simply typed lambda calculus

In Types as Abstract Interpretation, Patrick Cousot sketched how different type systems could be constructed from the collecting semantics of a language. However, the notation of the paper is very old ...

1
2 3 4 5
10