formal systems to specify properties of objects
1
vote
1answer
42 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 ...
11
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
314 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
46 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
40 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
32 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
35 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
32 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
60 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:
...
17
votes
0answers
138 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 ...
3
votes
0answers
31 views
Decidability of type inference and type checking in MLTT [migrated]
In Martin-Löf's An Intuitionistic Theory of Types: Predicative Part it is proved that type checking $a \colon A$ is decidable subject to $a$ being typeable in the first place, by proving a ...
1
vote
2answers
45 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
67 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
35 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
40 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
37 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
44 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
42 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
50 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
105 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
710 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
61 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
82 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
40 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 ...
3
votes
1answer
64 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
73 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
46 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
38 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
166 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
44 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
389 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
468 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
43 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
958 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
63 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 ...
3
votes
1answer
48 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
80 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 ...
3
votes
1answer
49 views
How should I describe the relationships between type expressions?
Lets say I have two type expressions: Maybe a (X) and Maybe Integer (Y), where Maybe is a ...
4
votes
3answers
88 views
Meaning of the notation Typ := TVar | (Typ → Typ)
In the paper "introduction to type theory" by Herman Geuvers, it states the following definition for the type theory of propositional logic (I've added "convention 2" just for reference):
Given ...
28
votes
4answers
2k views
What exactly is the semantic difference between set and type?
EDIT: I've now asked a similar question about the difference between categories and sets.
Every time I read about type theory (which admittedly is rather informal), I can't really understand how it ...
5
votes
1answer
93 views
Is there a formal difference between $f:X \to X$ and $f\in X \to X$?
We can denote by $X\to X$ the set of all functions from $X$ to $X$.
Therefore, we can use the following statement to say that $f$ is a function from $X$ to $X$:
$$f\in X\to X$$
But we usually state ...
6
votes
0answers
75 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 ...
0
votes
1answer
38 views
How to represent a map data structure mathematically
Wondering how to represent a map object such as the following mathematically:
var foo = {
a: 10,
b: 'bar',
c: true
}
You could say that it was a function ...
8
votes
2answers
324 views
How to derive dependently typed eliminators?
In dependently-typed programming, there are two main ways of decomposing data and performing recursion:
Dependent pattern matching: function definitions are given as multiple clauses. Unification ...
4
votes
1answer
143 views
What are some examples of types that can't be derived set theoretically?
I'm hoping for examples that aren't too abstract or useless in day-to-day programming, though not with a lot of hope, since in Bartosz Milewski's book, it is stated that generally speaking, the ...
4
votes
1answer
61 views
Agda: Which part does this type introduce universe inconsistency?
I was trying to prove following lemma,
...
0
votes
1answer
93 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 ...
2
votes
0answers
30 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 ...
