formal systems to specify properties of objects
0
votes
0answers
12 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’...
0
votes
0answers
18 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
27 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
45 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
41 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
48 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
37 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
79 views
Are Bad churches inhabited?
In type theory, some inductively defined data types allow you to prove absurdity. For example
...
1
vote
2answers
41 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
54 views
1
vote
0answers
27 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
33 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
55 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 ...
2
votes
2answers
372 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
49 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
43 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
36 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
62 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
302 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
47 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
104 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
40 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
41 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
44 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
46 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
48 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
51 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
107 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
713 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
74 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
80 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
84 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 ...
-1
votes
2answers
43 views
Defining an HTML Template as an Algebraic Type
Wondering if/how you could define a highly nested structure as a Dependent Type (or an Algebraic or Parameterized type). Specifically, an HTML template. Not that they work like this (HTML templates ...
4
votes
1answer
83 views
Dependent Type Theory Implementation of a Graph
In Haskell you find graphs defined like this:
data Graph a = GNode a (Graph a)
Or this:
...
5
votes
1answer
74 views
Pure type systems and let-expressions
I can not find any simple and detailed source of how to add non-recursive let-expressions to pure type systems.
The best I found is the Henk paper by Simon Peyton Jones, but his explanation of this ...
0
votes
1answer
51 views
How CompCert “proves” different things in its codebase
In order to understand examples of formal proofs, I am interested in how CompCert applies "proof" techniques. Specifically, I am wondering what a particular example is of something CompCert "proves" ...
0
votes
1answer
43 views
Meaning of $\mu t$ terms in dependent type theory
What is the meaning of the term $\mu t$ in the type theory formalized in this paper (section 2.1, page 2)?
2
votes
2answers
178 views
Confusion about the definition of de Bruijn terms in the TAPL book
I'm working through Types and Programming Languages right now, and I'm a little confused about the recursive definition given for nameless/de Bruijn terms (chapter 6, definition 6.1.2). Below is the ...
2
votes
1answer
46 views
What does “terms evaluated in related environments yield related values” means in the context of typing judgements?
I am reading Theorems for free! by Philip Wadler which is a paper about how to derive theorems from the type signature of a function.
Parametricity is just a reformulation of Reynolds’ abstraction ...
2
votes
1answer
38 views
Restrictions needed on ADT for totality
In the paper Total Functional Programming by D.A. Turner three rules are given for a programming language to remain total:
complete case analysis
covariant type recursion (type constructor should not ...
3
votes
1answer
394 views
How to Efficiently Define the Natural Numbers in Type Theory
A while ago I wondered about how Proof Assistants like Coq prove $m \leq n$ and the like. It looks like they actually need to traverse the natural numbers based on the successor/predecessor ...
7
votes
1answer
475 views
Is Coq synthetic or analytic?
In CMU's HoTT course, lecture 1, which can be found here: https://scs.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=0945cc7f-48b7-4803-81af-e7193a3f461d
At 33:52, Harper was giving parallel ...
1
vote
0answers
50 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 ...
4
votes
2answers
961 views
Understanding the Reasoning Behind These Typing Rules
So the expression $\Gamma \ \vdash \ e:\sigma$ states that under assumptions $\Gamma$, the expression $e$ has type $\sigma$. Then we have the following rules:
\begin{array}{cl}\displaystyle {\frac {x:...
3
votes
2answers
66 views
The difference between a Hoare Triple/Assertion and a Typed Function
I have been trying to wrap my head around applying Hoare Logic and am running into the question of how Hoare triples are any different from (simply) a typed function.
That is, say you have a typed ...
4
votes
1answer
50 views
When do we need U(n+2) to solve a problem that can be formulated in U(n)?
I understand the need for a universe hierarchy, and that each new level brings additionnal proof-theoretic strength.
In the HoTT book there are examples of proofs that need to use the next level in ...
2
votes
1answer
82 views
Assertion of Type Inference Rules/Type Checking
I have a problem in a book I am trying to accomplish.
I understand the overall type of the expression is boolean and how it derives. (y * x) will be rule 4 (counting from top right). (y * x) + x when ...
