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

3
votes
1answer
154 views

Algebraic data types - unions

Are there any programming languages where algebraic data types can be expressed not only by using intersection and disjoint union but also a standard set union (intersection + disjoint union)? Do ...
4
votes
1answer
166 views

how type checking fails?

I was doing a type checking example in system f sub on paper to understand how it works. according to Pierce's book Types and Programming Languages, numbers and their types are following in system f ...
8
votes
1answer
159 views

Relation between Type Assignment system (TA) and Hindley-Milner system

Recently I started my studies in type theory/type systems and Lambda Calculus. I have already read about Simple Typed Lambda Calculus in Church and Curry style. The last one is also known as Type ...
13
votes
2answers
466 views

Reference request: Category theory as it applies to type systems

I keep hearing about how one must learn category theory to truly understand programming language theory. So far, I've learned a good deal of PL without ever stepping foot into the realm of categories. ...
3
votes
0answers
103 views

What is the semantic model of types?

By reading literature on (denotational) semantics of types, I see that people tried to give several models of types. Reynolds showed that types in general cannot be given a set semantics in classical ...
4
votes
1answer
36 views

What is a “name/variable of base type” in applied $\pi$-calculus?

I'm studying the articleVerifying privacy-type properties of electronic voting protocols which uses Applied $\pi$-calculus to formalize voting protocols and verifies some privacy-related properties. ...
3
votes
1answer
84 views

What is the eta-rule for nat?

As far as I am aware of, the beta-rule of the natural numbers type nat states that (please correct me if I am wrong) ...
27
votes
2answers
3k views

Why is C's void type not analogous to the empty/bottom type?

Wikipedia as well as other sources that I have found list C's void type as a unit type as opposed to an empty type. I find this confusing as it seems to me that <...
3
votes
2answers
197 views

MLTT not being Turing Complete

Where can I find a proof that Martin-Löf Type Theory isn't Turing Complete, if such proof exists?
6
votes
1answer
187 views

Safe way to explicitly define new types instead of using Algebraic data types for my functional language

Question: As I'm working on a Hindley-Milner typed lambda calculus, in order to make it usable I need to add some types such as list and pairs. The way I currently do it is, I have an ...
4
votes
3answers
217 views

How Types avoids Russel's Paradox?

I gone through the Russel's paradox. From Wikipedia : According to naive set theory, any definable collection is a set. Let R be the set of all sets that are not members of themselves. If R is ...
5
votes
1answer
146 views

Does Damas-Milner still have principal types if existential type schemata are added?

In the Damas-Milner type system, type schemata can be formed in two ways: $T$ $\forall X. S$ Where $T$ ranges over monotypes and $S$ ranges over type schemata. The type-checking algorithm for this ...
0
votes
0answers
74 views

Set Levels in MSOL

I'm trying to see how Martin Lof Type Theory can be encoded in Monadic Second Order Logic over trees or graphs. Specifically, how can set levels (cumulative hierarchy) a la Russel or a la Tarski be ...
4
votes
2answers
336 views

System f-sub, how to do type checking?

I was reading that system f-sub (polymorphic lambda calculus with sub-typing) and I was quite confused with its one checking rule called "T-TAPP". This rule as following (ctx denotes the typing ...
7
votes
1answer
265 views

Is there any difference between extensible records and dependent maps

In a typed setting, records can be thought of as a map from field to type. If there is a well-typed record merge operation (which allows overlapping fields), is there any real difference between the ...
7
votes
2answers
286 views

Type-system combining type-states and typed effects?

Has anyone succeeded in implementing or designing a type-system that combines both type-state (linear types) and effect types (e.g. Koka)?
7
votes
0answers
182 views

Are type constructors always injectives even in presence of quantified type variables (subtyping)?

Are type constructors, in a language that feature subtyping and quantification of type variables, like scala or Java, always injective? That is, is an equivalent of haskell ...
6
votes
2answers
169 views

Is there a relationship between “sound and complete” in logic and “type safety” in PLs?

I've been wondering if there's a connection between "good logics" and "good programming languages". It seems that logics are shown to be "locally sound and complete" whereas programming languages are ...
1
vote
2answers
104 views

The range of significance in Type Theory

What exactly does "Types as ranges of significance of propositional functions. In modern 
terminology, types are domains of predicates" mean? Update: I found in this paper (Pag 14 or 234) by Russell, ...
8
votes
1answer
123 views

Origin of the concept of types

About the state of art that I'm running ahead of Type Theory I have the these questions all related about history of Types. Where did the idea of Type come from? (It seems that all start when ...
0
votes
1answer
92 views

Indexing a dependent type on a value?

If i'm recalling from Robert Harper's lectures Homotopy type theory A dependent type is a family of type index by a type. If we allow index to be just a value can we gain something instead of allowing ...
1
vote
0answers
58 views

DML , ML with restricted dependent types

Refering to this paper Dependent ML: An Approach to Practical Programming with Dependent Types Have defined datatype 'alist ( int ) Its not clear why they have used int as a parameter rather than a ...
5
votes
2answers
629 views

Strict positivity

From This reference : Strict positivity The strict positivity condition rules out declarations such as ...
4
votes
1answer
352 views

Family of types in type theory

Can anyone simplify the meaning of families of types index by a type. It looks i get it but quite not understood it. What do you mean by a "family" ? I understand index by a value (n length sequence)...
3
votes
2answers
76 views

Meaning of , and ; in relation to defining context

I have seen use of , and somewhere use of ; when defining context : $$\dfrac{\phi \ , \ \Gamma \ \vdash } {} $$ somewhere else i have seen : $$\dfrac{\phi \ ; \ \Gamma \ \vdash ...
5
votes
4answers
175 views

How to use Type application Rule to get a desired type

In type application Rule : $$\dfrac{ \Gamma \vdash t_1 : T_{11} \to T_{12} \qquad \Gamma \vdash t_2 : T_{11}} { \Gamma \vdash t_1 \ t_2 : T_{12} } \textsf{ (T-App)}$$ if we ...
0
votes
0answers
321 views

Type inference and Type checking

I understand that adding the annotations (dependent typing) may cause the type checking of the programming language to become undecidable. What about type inference ? Whether type checking and type ...
8
votes
1answer
121 views

Why is `map insertionsort` not to equal to`map mergesort`?

In the type theory podcast ep. 3, Dan Licata claims that the fact that for every input, insertionsort and mergesort give the same result does not imply that the result would be equal when used as ...
2
votes
1answer
110 views

Variable rule in dependent type theory

This is the = Type variable rule that I'm seeing through out the my course and unable to grasp it completely. $$\dfrac{\phi \vdash \Gamma[\mathrm{ctx}] \qquad \Gamma(x) = \tau} {\phi; \Gamma ...
5
votes
1answer
137 views

How precise is the statement “STLC is the internal language of CCCs”?

I'm studying some basic category theory in the context of type theory and came across the statement "simply typed lambda calculus is the internal language of cartesian closed categories". However ...
17
votes
2answers
381 views

“Minimal” intuitionistic type theory?

I'm surprised that people keep adding new types in type theories but no one seems to mention a minimal theory (or I can't find it). I thought mathaticians love minimal stuff, don't they? If I ...
5
votes
1answer
197 views

Proving preservation under substitution System F Omega

I am going over the proofs for the simply typed lambda calculus in the book "Types and Programming languages" by Benjamin Pierce. I am trying to find inspiration for the similar proofs for System F ...
7
votes
1answer
149 views

Difference between “sort” and “universe”

A very basic question. As title, what is the difference between "sort" and "universe" in type theory? Are they interchangable? Or are there only finite number of sorts, but infinite universes?
7
votes
2answers
315 views

Generating constraints to solve dependently-typed metavariables?

In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments....
3
votes
1answer
77 views

premiss of reduction rule (abst) of pure type systems

$$(abst) \:\frac{\Gamma, x: t_1 \vdash t_2: t_3 \quad \Gamma \vdash (x: t_1) \to t_3: s}{\Gamma \vdash (x: t_1. t_2): (x: t_1) \to t_3}$$ In this rule, why is $(x: t_1) \to t_3$ required to be an ...
1
vote
2answers
245 views

Program interpretation for static analysis

Are there any implementations, or even academic work, regarding an application capable of looking at code and inferring what the code actually intends to do? For example, we give it a program that ...
2
votes
0answers
24 views

Where does the term “Amechanicity” for type-error generation come from

I've been looking at these slides about improving type error messages for programming languages. One of the things they describe, starting at Slide 8, is the concept of amechanicity. Anytime the ...
3
votes
0answers
74 views

Describe data structure using equations

Good afternoon. At work I'm currently developing a system which takes user input (well structured) and then stores it in memory to do some processing. The input is basically a dataset formed by ...
6
votes
2answers
152 views

What does Harper mean by “class”?

I've been teaching myself type theory on and off over the past couple years. I've reach large sections of Pierce's Types and Programming Languages and Harper's Practical Foundations for Programming ...
10
votes
2answers
735 views

Universal/existential quantification?

I'm struggling to understand the purpose of universal and existential quantification of types. I'm playing around with writing a toy language based on the calculus of constructions. I've been reading ...
6
votes
1answer
362 views

Typing dependent pattern matching

I'm curious on how to type a dependent pattern matching in a functional language. What should the rule for typing ...
1
vote
1answer
122 views

What is the Haskell-style type signature called (i.e., who is it named after)?

A type signature in Haskell is written in the following format: functionName :: (arg1Type, arg2Type) -> returnType There's a (hyphenated, after a person or ...
9
votes
2answers
279 views

Proving a sorting operation in type system

I want to know how far a type system in a programming language can be beneficial. For example, I know that in a dependently typed programming language, we can create a ...
7
votes
1answer
152 views

What is the difference between ∀ and Π in the Calculus of Constructions?

As I've learned, the Calculus of Constructions has only two binders - $\lambda$ and $\Pi$. Morte, for example, has $\forall$ as a mere alias of $\Pi$. Yet, on the paper Self Types for Dependently ...
2
votes
0answers
47 views

What is the intuition behind a λ-term being EAL-Typeable?

λ-terms can be split in two categories: EAL and non-EAL typeable terms. It is known not only that EAL-typeable terms can be reduced to normal form in polynomial time, but that the reduction can be ...
9
votes
1answer
274 views

Do Self Types make the Calculus of Inductive Constructions obsolete?

Self Types are an extension of the Calculus of Constructions [1] that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
2
votes
1answer
126 views

Why do we distinguish between term abstraction and type abstraction in System F?

In System F, we distinguish between types and terms. Types are defined by the following BNF: \begin{align} A, B ::=&~\alpha && \text{(type variable)} \\ &|~A \rightarrow B &...
4
votes
1answer
263 views

What does Godels Incompleteness theorem “true but unprovable” mean?

I have asked this on the "computer science chat" ( vzn tried to explain me ) . I even watched a couple a videos to understand the theorem but still cannot convince myself. The following is the way the ...
3
votes
1answer
67 views

What is a proof of normalization of Morte?

It is said that any term on the calculus of construction halts. I am studying it through Morte, which is a bare bone implementation of the coc available on github. Is there any simple proof of ...
31
votes
3answers
743 views

What is a brief but complete explanation of a pure/dependent type system?

If something is simple, then it should be completely explainable with a few words. This can be done for the λ-calculus: The λ-calculus is a syntactical grammar (basically, a structure) with a ...