Questions tagged [type-theory]

formal systems to specify properties of objects

99 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
23
votes
0answers
764 views

Can a calculus have incremental copying and closed scopes?

A few days ago, I proposed the Abstract Calculus, a minimal untyped language that is very similar to the Lambda Calculus, except for the main difference that substitutions are ...
13
votes
0answers
201 views

Why do we have to forbid non-conforming lower and upper type bounds?

(it's a repost of my unanswered question from scala-user@googlegroups.com about Scala) In the Scala Language Specification, §4.4 Type Parameters, there is a requirement: The most general form of a ...
10
votes
0answers
515 views

Advantages of algorithm W over algorithm J for type inference in Hindley-Milner type system

According to A modern eye on ML type inference Furthermore, for some unknown reason, W appears to have become more popular than J, even though the latter is viewed—with reason!—by Milner as ...
8
votes
0answers
140 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, ...
7
votes
0answers
236 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 ...
7
votes
0answers
544 views

Main differences between intuitionistic type theory and calculus of constructions (CoC)

Quoting Wikipedia "Many systems of type theory, such as the simply-typed lambda calculus, intuitionistic type theory, and the calculus of constructions, are also programming languages." I'm a Coq user ...
6
votes
0answers
73 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, ...
6
votes
0answers
594 views

Is the strictly positive condition in Coq and Agda an aproximation?

Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a ...
6
votes
0answers
97 views

Bounded existential polymorphism

In his "Types and Programming Languages", Pierce, at the very end, presents the most powerful system in the book: $F^{\omega}_{<:}$. He, however, does not explain how bounded existential ...
5
votes
0answers
49 views

Rules for consistency with mutual inductive families?

I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other: ...
5
votes
0answers
446 views

Row polymorphism extended to modules

One common observation in type systems is that having subtyping makes type inference hard [1]. Consequently, for records, many modern functional languages shun subtyping (OO style) in favor of row ...
5
votes
0answers
87 views

How could one write typing rules with variables defined at call-site?

I'm trying to write typing rules for a simple language, which is basically a lambda calculus with SSA-like $\phi$-nodes, which basically exchange formal parameters for actual parameters. For ...
4
votes
0answers
56 views

Isomorfism between inductive and coinductive types (through double negation)

The paper "CPS Translating Inductive and Coinductive Types" mentions that there is an isomorphism between inductive (mu) and coinductive (nu) types, which they use for their translation. It states ...
4
votes
0answers
48 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 ...
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 ...
3
votes
0answers
38 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 ...
3
votes
0answers
57 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 ...
3
votes
0answers
92 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
0answers
37 views

On the diamond property for $F_{\omega}$ in TAPL

In page 455, of Pierce´s TAPL and page 560, the single-step diamond property of reduction: $S \Rrightarrow S' \land T \Rrightarrow T' \implies \exists V. T \Rrightarrow V \land U \Rrightarrow V$ ...
3
votes
0answers
28 views

What the type of an overloaded function should be?

Anecdotally, Virgill III language forbids overloading since overloading resolution is at odds with the language support of functions as first-class citizen, when resolution can't happen at compile ...
3
votes
0answers
74 views

Does Hindley-Milner refer to the unification algorithm for type reconstruction, a type system, or a form of polymorphism?

What does Hindely-Milner refer to? In Types and Programming Languages by Pierce, I only find that Section 22.4 Unification mentions "Hindley" and "Milner", when introducing the unification algorithm. ...
3
votes
0answers
74 views

Calculus of constructions, type-in-type and recursion

Does adding type-in-type to the calculus of constructions lead to (general) recursion? Such that one can write the Y combinator.
3
votes
0answers
33 views

Is the expression (λx.xx)(λy.y) typeable in the following system?

We are given a simple functional language: $ e ::= x | n | e_{1}e_{2}|\lambda(x:\tau).e$ with types: $\tau ::= \text{int} | \tau_{1} \rightarrow \tau_{2}| \tau_{1} \land \tau_{2} $ Is the ...
3
votes
0answers
84 views

An Alternative History of Haskell: being lazy without class?

[The q is a play on the title of this 2007 survey of Haskell.] tl;dr I have a couple of connected questions about Haskell's overloading mechanisms. I'll ask first then explain why. I'm looking at the ...
3
votes
0answers
131 views

PL: How can I prove the type of something using “Inversion for Typing”?

I'm currently going through this book about programming languages, and in section 4.2, Lemma 4.2 it says this: Lemma 4.2 (Inversion for Typing). Suppose that $\Gamma \vdash e : \tau$. If $e = \texttt{...
3
votes
0answers
149 views

Semantic parsing with Grammatical Framework - is this possible?

So far I have learned about categorial grammars, type logical grammars and formal semantics of natural language, the relevant tools are Cornell Semantic Parsing Framework https://github.com/clic-lab/...
3
votes
0answers
116 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 ...
3
votes
0answers
102 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 ...
3
votes
0answers
72 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 ...
3
votes
0answers
805 views

Row polymorphism, union and intersection types

It seems that row polymorphism with union types can be used in dynamic languages to approximate overloading, e.g. given the following python function: ...
3
votes
0answers
130 views

Test cases for subtyping with dependent types

I implemented a simple type system inside Agda and I'm trying to understand, how expressive it is. The system consists from a predicative hierarchy of universes in the style of Russell, natural ...
3
votes
2answers
116 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 ...
2
votes
0answers
42 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 ...
2
votes
0answers
28 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
75 views

How does the undecidability of Extensional Martin-Löf Type Theory apply to real type-checking compilers?

It is claimed in many sources (for example, here) that adding a rule like "if Id(X,Y) then X really equals ...
2
votes
0answers
48 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 ...
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: ...
2
votes
0answers
24 views

Is possible to construct a fixed set of typeclases as powerful as unconstrainde typeclasses?

We can construct a fixed set of combinators with a computational power equivalent to lambda calculus. Can we do the same with typeclasses (ad-hoc polymorphism)? For example, construct a finite set ...
2
votes
0answers
59 views

Are the permutation or weakening lemmas needed for term substitution?

In TAPL book, page 453, Pierce discusses the following lemma: $\Gamma , x:S , \Delta \vdash t:T \land \Gamma \vdash s:S \implies \Gamma, \Delta \vdash [x \mapsto s]t:T$ He claims that when $t$ is ...
2
votes
0answers
92 views

How could 'Complete and Easy Bidirectional Type Checking' handle invariant parameters on type constructors

The paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism provides examples for checking if one function type is a subtype of another, which I think demonstrates checking ...
2
votes
0answers
61 views

Simulating extensible sums with dependent types?

ML-style languages have a concept of "extensible" or "open" sum types, where variants can be declared at any point, and there's not a fixed number of constructors for the type. They're usually used to ...
2
votes
0answers
41 views

Real world example of contraction and weakening

Can you provide me a real world example of contraction and weakening in the type system of a popular language like Java, Kotlin, etc.? I heard that Rust has got explicit contraction but I don´t ...
2
votes
0answers
153 views

Proving that the failure of algorithm W implies that the program is not typable

How one does prove that if algorithm W failed for a given program $e$ and context $\Gamma$, then there is no substitution $S$ and type $\tau$ such that $S\Gamma \vdash e : \tau$ ? The original paper ...
2
votes
0answers
36 views

Substituting a term for a variable in a context

At this link you can read Nicola Gambino's slides on one way to approach the formal syntax of Martin-Löf dependent type theory. (They are concise and very readable.) On slide 10, he gives a standard ...
2
votes
0answers
39 views

How can one flip a stream using corecursion

Following is the definition of codata stream: codata Stream where hd : Stream −> A tl : Stream −> Stream For simplicity I assume I have just a ...
2
votes
0answers
36 views

Question about let syntax in type systems

I'm on the Wikipedia page for Hindley-Milner type systems, on the section about "let polymorphism": https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Let-polymorphism I'm a bit ...
2
votes
0answers
87 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
0answers
41 views

What is the difference between ADTs and ASDLs?

ASDL stands for Abstract Syntax Description Language (ASDL), whereby ADT stands for Algebraic data type. By looking at Python.asdl it appears to me to be the same thingy, just with different names, ...
2
votes
0answers
67 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 ...
2
votes
0answers
105 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, ...