Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [type-theory]

formal systems to specify properties of objects

8
votes
0answers
115 views

Extensional constructs in minimal extensional type theory without eta equality

The extensional version of Intuitionistic Type Theory is usually formulated in a way that makes extensional concepts like functional extensionality derivable. In particular, equality reflection, ...
2
votes
0answers
62 views

Examples of continuations in pure mathematics [closed]

I am not a computer scientist and have no knowledge of programming. However, I wondered continuations occur as natural and interesting mathematical structures, perhaps as algebraic or type theoretic ...
7
votes
1answer
104 views

Can literals in functional languages be thought of as functions from the empty type?

A while ago, I think on Stack Overflow, I saw someone say that Haskell literals can be thought of as functions that don't operate on anything. This makes sense to me but I remember someone else ...
4
votes
2answers
154 views

What is a fixpoint?

Could someone please explain me, what is a fix point? I caught the minimum explanation about fix point from the website: After infinitely many iterations we should get to a fix point where ...
3
votes
1answer
105 views

Partial type inference for dependent types

I'm looking for resources on (partial) type inference for dependent types. For example there could be a type inference scheme that fails if the term doesn't have a principal type, or a scheme that ...
7
votes
1answer
771 views

Cubical type theory for dummies?

I read one of those popular papers on cubical type theory, but no wonder I could only see formulas and diagrams without being able to recognize them at all. So here's what I want. I want a deep ...
1
vote
0answers
41 views

Formal name of the product of product type

What is the formal name in type theory of the operation that creates a "matrix of types" from product types (such as std::tuple in C++)? For example if we consider ...
4
votes
1answer
97 views

What is the difference between $x:A$ and $x \Xi A$?

Given a type hierarchy $(\tau,\sqsubseteq)$ and a signature $(VSym, FSym, PSym, \alpha)$, one says that the typing function $\alpha$ assigns to each variable symbol $x \in VSym$ a non-empty type $A \...
1
vote
0answers
22 views

Expressing Notion of Type “Scale”

I am looking for the terminology/concepts which express the nontechnical notion of the "layer" structuring of programs, the languages in which they are written, and a formal type theory. For instance,...
18
votes
2answers
634 views

Is there a non-trivial type which is equal to its own derivative?

An article called The Derivative of a Regular Type is its Type of One-Hole Contexts shows that the "zipper" of a type—its one hole contexts—follow the differentiation rules in type algebra. We have: ...
6
votes
1answer
353 views

What fragment of Martin-Löf dependent type theory can be expressed using generic types in Java?

I have recently come to realize that a number of problems I had a few years ago trying to implement various mathematical theories in Java came down to the fact that the typing system in Java is not ...
3
votes
1answer
102 views

partial (and non deterministic) functions in dependently typed lambda calculus

A partial function is one, that that is only defined on a part of its domain. Haskell gives examples: https://wiki.haskell.org/Partial_functions My end goal is to express types $$ \prod_{D:\mathcal{...
7
votes
2answers
610 views

Higher-ranked polymorphism without explicit application or subtyping?

So, I'm familiar with two main strategies of having higher-ranked polymorphism in a language: System-F style polymorphism, where functions are explicitly typed, and instantiation happens explicitly ...
7
votes
2answers
639 views

Relation between type-checking decidability, typability decidability and strong normalization

Yo! This is probably a stupid question, however I've never seen it written down explicitly if, for instance, decidability of type-checking is equivalent to the strong normalization property. Therefore ...
6
votes
0answers
56 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
3
votes
2answers
287 views

Which type compilers report if they cannot infer a precise type?

In the presence of subtyping, a type checker can usually infer only some inequality constraints on the type rather than the exact type. Of course, internally it will store the full constraints. But ...
5
votes
1answer
91 views

Local type argument synthesis when type variable does not appear in arguments

I am implementing the techniques described in the classic Local Type Inference paper. Specifically, I am implementing the type argument synthesis algorithm from section 3. My algorithm seems to ...
5
votes
1answer
121 views

Functorial type constructors in System F

I have come across the claim that all basic data types in System F, such as Bool, Nat, and List(U), can be expressed in the form $\forall \alpha (((T\alpha \rightarrow \alpha) \rightarrow \alpha)$, ...
2
votes
1answer
327 views

Type Theory and Principia Mathematica Part IV “Relation Arithmetic”

As type theory is a principle focus of modern computer science, its origins are in Bertrand Russel's theory of types, Principia Mathematica is both the origin of and is expressed in the theory of ...
2
votes
1answer
127 views

Construct a proof tree in Hindley-Milner with function overload

I'm reading Wadler's paper called "How to make adhoc polymorphism less ad hoc". I'm trying to understand the given rules for function overload (over and inst) and I want to create a small example of a ...
6
votes
2answers
236 views

What cannot be proven at compile-time about a computer program?

Is there a Turing-Complete-ish programming language without runtime errors? Like segmentation faults, memory leaks, race conditions, deadlock/livelock/starvation, etc.? With strongly typed languages, ...
4
votes
0answers
44 views

Subtyping relationship in a simple type system

This example is from Algebraic Subtyping, p. 14. Let's say we have a type system with just function types, $\bot$ and $\top$; propositions involving type variables are defined by quantification over ...
9
votes
1answer
100 views

Can a type system serve as a proof assistant for foreign functions?

Given that: A language with very expressive type systems (e.g. Idris) can also have escape mechanisms like foreign function interfaces/unsafePerformIO. There are proof assistants that can be used to ...
2
votes
0answers
55 views

Uniqueness typing

In Uniqueness Typing Simplified, when applying functions, how many times the function could be used is simply ignored , however, in I Got Plenty o’ Nuttin’ , the application inherit the sparsity ...
6
votes
3answers
297 views

Proving property of a term using Induction

This is one of the example lemma that has been proved in TAPL book which I'm unable to grasp. The objective is to prove |Consts(t)| <= size(t) where ...
3
votes
1answer
110 views

Distributive property with sum types and product types

In Philip Wadler's presentation, "Category Theory for the Working Hacker", something confused me. At about 30:52, he says: We need this additional construct which is called distributivity. Here it ...
13
votes
1answer
236 views

Is the derivative of a graph related to adjacency lists?

Some of Conor McBride's works, Diff, Dissect, relate the derivative of data types to their "type of one-hole contexts". That is, if you take the derivative of the type you are left with a data type ...
3
votes
2answers
632 views

forall a b, a -> b [duplicate]

I know for pretty sure that there is a function with the type $f: \forall \alpha, \beta . \alpha \rightarrow \beta$ (at least in a Hindley-Milner type system), but I can't wrap my head over it. ...
3
votes
1answer
119 views

Is it possible that the universe of types could be closed?

I asked a pretty vague question. I wasn't able to make it precise, but I can now. It seems to be out of the scope of the previous question, so I open another one. In dependently-typed languages such ...
1
vote
1answer
30 views

Clarifying “operation” in the definition of data type

A definition of data type I've seen is along the lines of "a set of values and a set of operations". What exactly does an operation in this set comprise? For instance, might an operation be ...
7
votes
1answer
381 views

Recursive type encoding on System F (and other pure type systems)

I am studying pure type systems, particularly the calculus of constructions, and trying to use an encoding for recursive types on it, which, according to Philip Wadler, is possible. As an example, I'm ...
2
votes
1answer
84 views

Is there a correspondence between the syntaxes and the type systems of programming languages?

I was reading the first chapter of Robert Harper's Practical Foundations for Programming Languages in which it introduced abstract binding trees, aka abt. It seems pretty like typed lambda calculus. ...
10
votes
1answer
220 views

Why are recursive types needed as primitives for proofs in dependent type systems?

I'm relatively new to type theory and dependent programming. I've been studying the calculus of constructions (CoC) and other pure type systems. I'm particularly interested in using it as a proof-...
9
votes
1answer
169 views

What is a super universe?

I'm reading this well-known paper On Universes in Type Theory. At first I expected something similar to Setω in Agda, but it turns out that it's even something more ...
6
votes
1answer
353 views

Is it possible to copy data in a linear type system?

I'm having a little problem with the abstraction layers in linear types. If every variable is used exactly once, there is no way to copy data, since you have to read each datum twice in order to write ...
2
votes
0answers
82 views

Dependent types as regular expressions

Would be possible to encode dependent types as regular expressions? if so, ¿is there some work about? It's common to represent restrictions for elements in a traversable data structure with them, ...
5
votes
1answer
181 views

How do I interpret the wording of this passage about abstract binding trees from the book Practical Foundations of Programming Languages

On page 7/8, section 1.2, of Practical Foundations of Programming Languages, 2nd edition, Robert Harper gives this initial definition of abstract binding trees: The smallest family of sets closed ...
8
votes
2answers
154 views

Domain Theory and Polymorphism

Domain theory gives an amazing theory of computability in the presence of simple types. But when parametric polymorphism is added there doesn't seem to be a nice theory that explains whats going on ...
2
votes
1answer
269 views

Why aren't existential types implemented in any mainstream language?

I'm talking about first-order existential types, as summarized here, with pack as the introduction form that bundles up a type with an expression of that type, and <...
11
votes
1answer
129 views

Can properties such as memory usage of a function be expressed in a dependently typed language?

Suppose one wants to reason about properties of code beyond things like totality and functional purity - one also cares about the memory consumption, or algorithmic complexity of a function. Can this ...
2
votes
1answer
65 views

Types and Types Systems concepts

Given this definitions about Types and Type systems : Types are described by means of a language of type expressions: Basic or primitive types: Bool, Char, Int, ... Type variables: a, b, c, ... ...
1
vote
0answers
50 views

Curry howard Isomorphism what the propositions A , B ranges over

In CH-I what the propositions A , B ranges over too ? An update : From Pfennings notes : "A denotes proposition about the mathematical objects such as integer or a real number." From : Per ...
1
vote
0answers
121 views

Curry howard isomorphism “proof as program”

I'm reading CH Isomorphism. Let's divide into two stages: Prop corresponds to types. so a proposition A $\wedge$ B corresponds to type A $\times$ B. Proof corresponds to the program. What is the ...
2
votes
1answer
85 views

Collection of inference rules viewed itself as a judgment

I'm confused about the intended meaning of the following passage from Bob Harper's Practical Foundations for Programming Languages: A collection of rules is considered to define the strongest ...
5
votes
1answer
402 views

Are there any type constructors which are *not* functors?

So I'm almost done teaching myself category theory. One of the main take-aways for me is that type constructors (higher-kinded types) are endo-functors. But it this always the case? What's throwing ...
3
votes
2answers
55 views

how to use type application rule (T-TAPP)?

In the following rule, $$\dfrac{ \Gamma \vdash t_1 : \forall X.T_{12} } { \Gamma \vdash t_1 \ [T_2] : [X \mapsto T_2]T_{12} } \textsf{ (T-TApp)}$$ whend doing type checking, how ...
4
votes
1answer
76 views

How to understand these exposure algorithm rules for System F sub?

The book "Types and Programming Languages" said System F sub type checking introduce exposure typing rules alongside algorithmic typing and sub-typing rules. ...
1
vote
0answers
91 views

Typing rules of coinductive types?

Are there typing rules for specific coinductive types such as conat or stream, or even in general the M-types?
9
votes
1answer
969 views

What is induction-induction?

What is induction-induction? The resources I found are: the HoTT book, at the end of chapter 5.7. nLab's article a paper called Inductive-inductive definitions this blog post also mentions inductive-...
3
votes
3answers
74 views

A question about type rule

I realized that almost no one explained how to selected the type variable T1 ...