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

4
votes
1answer
165 views
3
votes
1answer
32 views

T&PL: Language grammar with terms

I'm autodidacting Pierce's Types and Programming Languages. On page 27 he states a definition for "terms, concretely" in constructing a language of terms, thus: For each natural number $i$, define a ...
1
vote
1answer
25 views

What is the difference between a Top type and a Unit type

Wikipedia defines a Top type: (edited for readability) The Top type [...] is the universal supertype, as all other types in any given type system are subtypes of Top However, the article goes on ...
1
vote
0answers
16 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?
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 ...
3
votes
1answer
168 views

Drawbacks of adding type equality to 1ML

In the 1ML – Core and Modules United (F-ing First-Class Modules) paper, the author gives the following example for why module types do not form a lattice under subtyping: ...
4
votes
1answer
138 views

Typing rule for binding groups

In "Typing Haskell in Haskell", by Mark P. Jones, is provided a sort of haskell-like specification for typing Haskell. As stated in this paper, binding groups is a area "neglected in most theoretical ...
0
votes
0answers
41 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 ...
3
votes
1answer
55 views

Is there a generally accepted name for creating types that select a subset of other types?

Tl;Dr; Given: type A = { int: foo, int: bar } type B = select foo from A What is the name of the typing relationship between A and B? What is the name of the ...
1
vote
0answers
22 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 ...
3
votes
1answer
63 views

Roadmap to formal verification

I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also ...
5
votes
2answers
110 views

LET REC recursive expression static typing rule

I'm taking a programming languages course and had a question regarding the typing rules for a recursive let rec expression in a static typing system. To be more ...
1
vote
3answers
92 views

Soundness and completeness w.r.t. programming languages

I'm studying programming languages (more specifically type systems) and came across a concept I couldn't quite wrap my head around: soundness and completeness. I'm taking a class, and according to my ...
0
votes
0answers
24 views

Composition of compostion as a functor

"Composition of Composition" (i.e., (.) . (.)) in Haskell), has type ...
1
vote
1answer
37 views

PL: What solves the type isomorphism $X \cong (X \rightarrow \mathbf{2})$?

In Practical Foundations for Programming Languages, on page 138 (page 156 of the pdf), it says: Requiring solutions to all type equations may seem suspicious, because we know by Cantor’s Theorem ...
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
1answer
36 views

Curry-howard isomorphism in object oriented programming languages

I want to get a better intuition for the curry howard isomorphism, and my intuition is mainly based on object oriented programming languages like JavaScript. So as an example, I am going to formalize ...
1
vote
2answers
56 views

What is the type signature of a Turing Machine?

Maybe my question is a bad question, but if it is, I want to know eactly how it is a bad question. Suppose we have some Turing machien $M$ that takes as input a natural number $n$ in the form of a ...
0
votes
1answer
46 views

Bounded Quantification: Full F<: intuition

I'm currently looking into Chapter 26 of Types and Programming Languages and am a bit confused by the "intuition" for Full F<: (p. 395): A type T = ∀X<:T1.T2 describes a collection of ...
2
votes
1answer
55 views

Does co-inductive and co-recursive types also have their recursors?

I'm new to type theory, and recently read introductory materials where dependent type are discussed. One of my friend asked me, "Those dependent types are having recursors & 'inductors'(dependent ...
3
votes
1answer
42 views

Multiplicative Pure Type Systems

All the references about Pure Type Systems I know consider only systems that allow to recover natural deduction systems with additive rules. Is there any variant that allows it to recover natural ...
3
votes
2answers
82 views

Are Bad churches inhabited?

In type theory, some inductively defined data types allow you to prove absurdity. For example ...
1
vote
2answers
44 views

How can MLTT etc encode computability?

I am recently thinking about proving the undecidability of some problem. This problem has been formalized in Coq and by staring at it, people including me think "for sure" this is undecidable. "For ...
2
votes
2answers
82 views
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, ...
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-...
1
vote
1answer
58 views

Is there any sort of formal definition of terms like 'data type', 'abstract data type', etc?

If not (because I assume not) is there some kind of reference or book that provides some theoretical foundation to these concepts? I've been learning about data structures and abstract data types for ...
12
votes
4answers
2k views

What does the leading turnstile operator mean?

I know that different authors use different notation to represent programming language semantics. As a matter of fact Guy Steele addresses this problem in an interesting video. I'd like to know if ...
3
votes
2answers
381 views

What makes a proof assistant a proof assistant?

You open a code editor, define a syntax with lambdas, a few primitives. Then you invent some nice computation rules, some cool typing rules, and write a corresponding interpreter and "type checker". ...
1
vote
1answer
53 views

how to deduce a function subtype rule from a given function type definition

This question relates to liskov substitution principle seems to have two conventional meanings but is really a different question, so I'm posing it as a new question. I'm doing a bit of research into ...
2
votes
1answer
44 views

liskov substitution principle seems to have two conventional meanings

This is a question about the semantics of the name, rather than about the principle itself. What is the Liskov Substitution Principle (LSP)? LSP seems to have two meanings in the literature I've ...
1
vote
1answer
35 views

How to define the natural numbers as a W-type?

I'm having trouble understanding the rules for W-types in type theory as defined here: https://ncatlab.org/nlab/show/W-type#wtypes_in_type_theory Can someone give an example of how these rules could ...
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 ...
3
votes
0answers
46 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 = \...
7
votes
1answer
65 views

Flawed argument in the proof of function extensionality in cubical type theory?

I am reading the lectures about cubical type theory in this github repo. In lecture 1 the author defines function extensionality the following way: ...
19
votes
0answers
427 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 ...
1
vote
2answers
49 views

What is the use case of multi-type-parameters generic interface?

Previously, I ask a similar question, but the answer given only demonstrates the usage of multiple-type-parameters(MTP) data structure, but not MTP generic interface. Based on my experience, generic ...
4
votes
0answers
153 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 ...
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?
3
votes
1answer
42 views

Are all terms of type forall a. a operationally bottom?

Is there a proof that all terms of type $\forall{a}. a$ are operationally $\bot$, in a non-weakly-normalising version of System F? If you ask a free theorem calculator such as this one for the free ...
5
votes
1answer
60 views

Hindley-Milner type inference for language with implicit type casting

I've only implemented the HM algorithm on a small academic language with a few primitive types and functions. In that case, the unification algorithm would return a type error if two different ...
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 ...
2
votes
1answer
56 views

Induction on typing derivation in refinement types system

From the text Principles of Type Refinement page 14: The author introduces in definition 2.2.7 the rule: $$ \dfrac{\Pi \vdash t : R \qquad R \le S}{\Pi \vdash t : S} $$ and gives the following ...
0
votes
1answer
52 views

Can you automatically generate a parser for a type using type theory some how?

Was wondering since all the types are spelled out constructively, and the constructions can all be reflected symbolically on a computer, if you can automatically parse expressions in a type?
6
votes
1answer
116 views

Relationship between Higher Kinded Polymorphism, type inference, and Currying

On Hacker News there is an interesting exchange about the async\await RFC for Rust. The author of the proposal withoutboats is responding to a comment about the ...
4
votes
1answer
714 views

What is the use case for multi-type-parameter generics?

In C#, one can define a class/method/function with multiple type parameters. For example, ...
1
vote
3answers
76 views

What are the concequences of the unit type and the unit value being the same?

What are the practical and theoretical implications of the unit type and the unit value being the same or different entities? For example, in Haskell the unit type and unit value are both spelled <...
2
votes
1answer
91 views

What are the implications of Lean not having the type `Set`?

In Coq we have an impredicative base type, called Prop, and a predicative base type, called Set, both of type ...
5
votes
2answers
91 views

Definition of “properly partial” versus “total” value types

In the Foundations chapter of Elements of Programming (Stepanov and McJones, 2009), this paragraph appears: A value type is properly partial if its values represent a proper subset of the abstract ...