Stack Exchange Network

Stack Exchange network consists of 175 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

0
votes
0answers
69 views

Definition of M-type in type theory

According to nLab, M-types are the dual of W-types. What are the introduction and elimination rules for M-types? Edit: For example, the formation/introduction/elimination rules for W-types are: $$\...
2
votes
1answer
42 views

How to statically type polymorphic lambdas using hindley milner style type inference

I am playing with a simple implicitly typed functional language and have implemented type checking using a Hindley Milner style system. In order to guide code generation, I want to tag each term with ...
0
votes
1answer
61 views

Is it possible to interpret some Martin-Löf types as abelian monoids in such a way that any abelian monoid can be represented as a type?

For instance, I can interpret the unit type as the trivial monoid with one element. Non-dependent pairs $A \times B$ can be interpreted as the direct sum $A ⊕ B$ when $A$ and $B$ can both be ...
3
votes
1answer
44 views

Meaning of the “why not” modality from linear type theory?

In linear type theory there is a modality written ! where !T can be read as "infinite copies of ...
1
vote
1answer
141 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 ...
5
votes
3answers
67 views

How exactly do we define parametric polymorphism?

My naive distinction between parametric polymorphism and ad-hoc polymorphism, is that: In parametric polymorphism, the type is given as a variable: (pseudocode) Function f: <.Type T> T $\to$...
4
votes
2answers
129 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{...
2
votes
0answers
29 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 ...
1
vote
0answers
55 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 ...
5
votes
2answers
65 views

Identity types and universes

Let us consider Martin-Löf type theory with a cumulative hierarchy of universes $$ \mathcal{U}_0\colon\mathcal{U}_1\colon\ldots $$ If $A, B\colon \mathcal{U}_i$, we can form an identity type $A=_{\...
0
votes
0answers
21 views

If you can have cyclic base types, or if they need to be infinite types

I am confused how to properly think about classes of classes. Basically, you can have a dog "filo" which is an instance of the dog "class". But the dog class is itself not an instanceof of "animal", ...
2
votes
1answer
119 views

Dependent type system with different computation model

There exist various Turing-equivalent models of computation, such as lambda calculus, Turing machines, or register machines. It seems that dependent type systems (like Coq, Agda, Idris, homotopy type ...
5
votes
1answer
575 views

Where are C++ templates inside of the lambda cube?

C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or ...
3
votes
1answer
47 views

What are different ways to provide a semantics to a language?

Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I ...
2
votes
0answers
29 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 ...
1
vote
0answers
45 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
1answer
40 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 ...
3
votes
1answer
37 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
0answers
21 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
25 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 ...
4
votes
1answer
156 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 ...
7
votes
2answers
291 views

What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
3
votes
1answer
238 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: ...
0
votes
0answers
43 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
69 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 ...
3
votes
1answer
59 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 ...
13
votes
1answer
247 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 ...
1
vote
0answers
23 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 ...
5
votes
2answers
125 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
151 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 ...
1
vote
1answer
40 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 ...
0
votes
0answers
24 views
0
votes
1answer
114 views

Can the foundation of computer science be implemented to include new rules of inference so that computer can do causal reasoning?

The idea I'm thinking of is about a top-down approach for AI. I would like to know if there can be a model for computers so that they can perform causal reasoning. It seems that causal relation can be ...
1
vote
0answers
18 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
32 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
43 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
62 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
47 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
64 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 ...
6
votes
0answers
92 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 ...
3
votes
1answer
43 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
83 views

Are Bad churches inhabited?

In type theory, some inductively defined data types allow you to prove absurdity. For example ...
1
vote
2answers
46 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 ...
4
votes
0answers
42 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-...
2
votes
0answers
32 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
1answer
61 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 ...
3
votes
1answer
126 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 ...
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 ...
17
votes
4answers
2k views

Why must a function with polymorphic type `forall t: Type, t->t` be the identity function?

I am new to programming language theory. I was watching some online lectures in which the instructor claimed that a function with polymorphic type ...