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

19
votes
0answers
424 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
171 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 ...
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, ...
7
votes
0answers
143 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 ...
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
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, ...
6
votes
0answers
373 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
338 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
89 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
68 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
37 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
150 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 ...
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 ...
3
votes
0answers
37 views

Type system for Query DSL with only simple GADTs: what typing judgments are needed?

Background I have several F# codebases with reasonably high level of complexity of code. In order to convince myself that the code is solid I do whatever I can to write as much of it as possible type-...
3
votes
0answers
45 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 = \...
3
votes
0answers
73 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
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 ...
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 ...
3
votes
0answers
660 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
490 views

Encoding row types

I'm working on a type system with extensible records, similar to ones explained in "A Polymorphic Type System for Extensible Records and Variants - Benedict R. Gaster and Mark P. Jones" and "...
2
votes
0answers
36 views

How can I prove impossibility of generalizing a given higher order function from pure to monadic or applicative?

There is a great divide in Haskell between pure and monadic algorithms. While the latter are indistinguishable from their usual imperative counterparts, the former can get much more magical. What this ...
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 ...
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, ...
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 ...
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 ...
2
votes
0answers
94 views

Is there a formalization of automatic-splicing data structures?

I'm wondering if there is some formalization, type theoretical analysis, or similar for data structures that automatically "splice" in an associative way. Barring a perfect citation, I'd be interested ...
2
votes
0answers
114 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 ...
2
votes
0answers
56 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 Type Recursion, ...
2
votes
0answers
129 views

Are there models of type theory that allow the real numbers to be a type?

Do there exist models of type theory that allow types to contain an uncountable number of inhabitants? Traditionally type theory seems to be swirled in with computable programs as constructive proofs ...
1
vote
0answers
15 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?
1
vote
0answers
21 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 ...
1
vote
0answers
16 views

Propositional extentionality in the lean theorem prover?

Propositional extentionality in the lean theorem prover is stated as the following axiom: axiom proptext {a b : Prop} : (a $\iff$ b) \to a = b My confusion about this is as follows: Previously I’...
1
vote
0answers
28 views

Type theory based automated theorem prover?

I know that there exist type theory based proof-checker, and I know that there are logic/sequent-calculus based automated theorem provers. But I haven’t heard of a type-theory based automated theorem ...
1
vote
0answers
29 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, ...
1
vote
0answers
43 views

What's are the consequences of subject expansion property?

Subject reduction is a well and widely used property of typed rewriting systems. Subject expansion is much less known. What are the applications of this property and which systems enjoy it?
1
vote
0answers
51 views

On the termination of mutually recursive functions

In Finding Lexicographic Orders for Termination Proofs in Isabelle/Holl the authors construct a method for proving termination of functions based on constructing a matrix that registers for each row ...
1
vote
0answers
58 views

Combinatory logic equivalent to System F

Simply typed lambda calculus has a combinatory logic equivalent with the same expressive power without the need of defining names via lambda abstraction. Is there a formalism as powerful as System F ...
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 ...
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,...
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 ...
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?
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 ...
1
vote
0answers
66 views

Type systems understanding problems

I'm not sure if this is the correct place to ask this kind of a question, but here goes: I'm doing my own reading of the Principles of Program Analysis book, and i'm having trouble understanding some ...
0
votes
0answers
19 views

Computational type theorists: how do you compare terms for equality here?

I am attempting to implement Simple Type Theory in the language D. How do you compare subterms to a term $R$ for the sake of computing the covering abstractors of $R$ in $M$? By reference (class ...
0
votes
0answers
36 views

Mathematical resource material accompanying TAPL

I'm currently reading Types and Programming Languages by Benjamin C. Pierce and just arrived at chapter 21 Metatheory of Recursive Types. Prior to this chapter I found the book challenging but ...
0
votes
0answers
24 views

Composition of compostion as a functor

"Composition of Composition" (i.e., (.) . (.)) in Haskell), has type ...
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 ...
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 ...