Questions tagged [type-theory]
formal systems to specify properties of objects
477
questions
1
vote
2answers
62 views
Given an algorithm, is it possible to find all other equivalent algorithms for the same computable function in the same model
For any computable-function, there may be multiple different algorithms (possibly countably infinite). For example, sort has many different implementations/algorithms, that we know of or that we have ...
1
vote
1answer
53 views
Which would be better for programming using Homotopy type theory Agda or Idris
I'm looking to model data inputs for an artificially intelligent system, which is affected by its internal parts and has feedback loops. I'd like to model it mathematically, using category theory or ...
0
votes
1answer
58 views
How do real numbers like Pi, golden ratio, etc fit into type theory
In type theory, all computable functions must terminate, however, numbers like Pi are non-terminating real numbers, hence a non-terminating function is required to compute this number, even though one ...
1
vote
1answer
33 views
Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda
An observation when defining List in agda with --without-K enabled:
The following parameterized inductive definition is accepted:...
4
votes
3answers
313 views
How Types avoids Russel's Paradox?
I gone through the Russel's paradox.
From Wikipedia :
According to naive set theory, any definable collection is a set. Let R be the set of all sets that are not members of themselves. If R is ...
1
vote
1answer
53 views
Is there a relationship between visitor pattern and DeMorgan's Law?
Visitor Pattern enables mimicking sum types with product types. Where does the "sum"-iness come from?
For example, in OCaml one could define ...
2
votes
0answers
41 views
Do any industry programming languages use Martin-Löf style identity types?
Most programming languages have some kind of type systems but are there any programming languages widely used outside of academia (in consumer-oriented tech, finance etc.) that have intensional ...
3
votes
0answers
36 views
What's the relationship between “semantic type soundness” and “functional correctness”?
In the Milner Award lecture "The Type Soundness Theorem That You Really Want to Prove (and now you can)" and related Sigplan blog post (with collaborators), Derek Dreyer argues that semantic ...
1
vote
0answers
22 views
Interpreting Minimal STLC using a $\lambda 1$ Category
On page 139, example 2.4.5 of "Categorical Logic and Type Theory" by Bart Jacobs demonstrates the interpretation of the abstraction typing rule with respect to a $\lambda 1$ category. ...
16
votes
3answers
4k views
Which research languages have a stronger typesystem than Haskell and why?
Here I read that:
Haskell definitely does not have the most advanced type system (not
even close if you count research languages) but out of all languages
that are actually used in production ...
2
votes
1answer
75 views
How does the undecidability of Extensional Martin-Löf Type Theory apply to real type-checking compilers?
It is claimed in many sources (for example, here) that adding a rule like "if Id(X,Y) then X really equals ...
1
vote
1answer
69 views
Resources for implementing dependent type theory
I want to implement Martin Löf's intuitionistic type theory in a functional language such as Haskell, preferably also implementing a lexer/parser for the language. How should I start approaching it? ...
6
votes
2answers
166 views
Rigorous proof that parametric polymorphism implies naturality using parametricity?
This question asks for an informal explanation of why all polymorphic functions between functors are natural transformations (This is a claim made by Bartosz Milewski). One answer to that question ...
0
votes
1answer
35 views
Can we somehow get functoriality from purely type-theoretic reasoning?
In this question, I asked about how to prove naturality from parametric polymorphism, using parametricity. The current answer to that question simply assumes that the functors in question satisfy the ...
0
votes
0answers
16 views
Is there a uniform way of giving for any mathematical formula a hypercomputer that computes it?
Some mathematical formulas directly suggest an algorithm for computing it (even if sometimes an inefficient one).
For example, if we recursively define $\sum_{i=1}^nx_i=x_n+\sum_{i=1}^{n-1}x_i$, then ...
2
votes
1answer
38 views
What does $\text{dom}(\Gamma)$ mean in the context of an inference rule?
In the wikipedia page on pure type systems, it gives the following inference rule:
$\frac{\Gamma \vdash A : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : A \vdash x : A }\quad \text{(start)}$
...
1
vote
0answers
55 views
Resources for connections between dependent type theory and LCCC
Can someone recommend introductory articles/papers on the connections between dependent type theory and locally cartesian closed category? Many Thanks!
2
votes
1answer
59 views
Is a system of equations derived from mutually recursive ADTs always uniquely solvable?
After looking at Can a computer determine whether a mathematical statement is true or not? for a while, I worry we may be into incompleteness/halting problem territory with this question, so an answer ...
3
votes
2answers
116 views
How do you have a type typed “Type” when implementing a programming language?
I am working on the base of a language model, and am wondering how to represent the base type, which is a type Type. I have heard of an "infinite chain of ...
5
votes
2answers
755 views
Question on the “Tutorial implementation of dependently typed lambda calculus”
I have a slight technical struggle with this marvelous tutorial. On page 5 the tutorial talks about typing rules for Simply Typed Lambdas and presents following judgement as derivable via rules on ...
6
votes
1answer
803 views
Why product type is a dependent SUM?
It might just be a stupid question but I simply see no obvious reason why dependent sum type is a generalized form of product type. Concretely, the sigma type $\Sigma(x:S)T$ degenerates to a product ...
1
vote
1answer
117 views
Creating a large tuple from smaller tuples via a monad or applicative
Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term
$\lambda x_{\beta}. \;(x, \, ...
2
votes
1answer
64 views
Curry–Howard correspondence and functional programming “reliability”
The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness".
I recently ...
2
votes
2answers
108 views
Does any language need to have a bottom type?
From wikipedia:
In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also called the zero or empty type, and is sometimes denoted with the up tack ...
3
votes
1answer
81 views
What is an uninhabited type?
https://en.wikipedia.org/wiki/Type_inhabitation
The wiki article above says,
To be sound, such a system must have uninhabited types.
What is the definition an uninhabitated type? Do all programming ...
0
votes
0answers
29 views
Generalised letrec semantics for mutual recursion
I'm new to system types and I was wondering how mutual recursion is defined through generalized
e::= ..|let rec x1=e1 ,...., xn=en in e .What has to be added in the "simple" let rec ...
4
votes
0answers
75 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 ...
2
votes
0answers
28 views
How to specify mutated types mathematically?
Say I have an object which I pass to a method, and the method returns that same object, just mutated.
So it goes like this:
...
2
votes
1answer
57 views
Greatest fixpoint of the type of lists
I'm working through Samuel Mimram's book Program = Proof. In the first chapter, he discusses recursive types in OCaml, and inductive types. An exercise he provides on the topic has me a little bit ...
0
votes
0answers
47 views
What is the difference between type theory and logic programming (in terms of declarative programming and specification)
How is does type theory (coq, lean, agda), and logic programming (prolog, datalog) differ from each other.
Logic programming is a way of declarative specifying an algorithm, using classical 1st order ...
6
votes
1answer
287 views
Relationship between inductive families and type-returning functions
Dependently typed languages such as Agda support inductive families, also called indexed datatypes, which allow type parameters to vary between constructors. This can be used to define a set of ...
3
votes
1answer
70 views
Which language is used to construct a type system?
Typically, OCaml and Scala seem to be used for designing any programming languages tool. But what features offer them an edge over other languages.
A related question, is a type system for a language ...
4
votes
2answers
156 views
What are the implications of Homotopy Type Theory?
I've recently come across the topic of homotopy type theory and I'm interested to learn more. I have a very limited background in type theory.
Can anyone tell me, in functional programming terms or ...
3
votes
1answer
118 views
How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?
The well-known Church encoding of natural numbers can be generalized to use an arbitrary (covariant) functor F. The result is the type, call it ...
2
votes
1answer
69 views
What are the most used statements in programming (ranked)?
I was wondering if there are any resources for a study/ranking of the most frequently used statements (by statements I mean assigning, invoking, instantiating etc, like in C#) in programming overall (...
0
votes
0answers
29 views
Is the borrow checker mechanism in Rust based on quantitative types?
I was trying to understand if the borrow checking mechanism for references is actually a quantitaive type in disguise because it does look very similar. In case these are just similar but unrelated ...
2
votes
4answers
438 views
Is there such thing as “sequential types”?
I am wondering how you could possibly define the implementation of an imperative function as a type. Is it possible? Currently I only see the input parameters and output result used in the definition ...
Gilles 'SO- stop being evil'
40.3k7 gold badges108 silver badges171 bronze badges
1
vote
2answers
81 views
0
votes
0answers
87 views
Can we think of a non-symmetric product type in Haskell?
Meta note: I asked this question here a while ago. It got an answer:
type a /\!! b = (a, ((b -> Void) -> Void))
Unfortunately, I do not reckon it to be ...
1
vote
1answer
133 views
What's the difference between Row Polymorphism and Structural Typing?
The definitions I've stumbled across seem to indicate they express the same idea. That's that the relationship between record types is determined by their fields (or properties) rather than their ...
1
vote
1answer
39 views
Example of Dependent Types?
Say you have 3 objects, a global MemoryStore, which has an array of MemorySlabCache objects, and each ...
0
votes
0answers
65 views
Consistency of a set of bidirectional typing rules
Main
Is there any way to algorithmically check the consistency of a set of bidirectional typing rules, e.g. the absence of cycles and the uniqueness of the derivation tree? This problem is naturally ...
2
votes
1answer
77 views
Does canonicity imply weak normalization?
Context: type theory.
My understanding of:
WN: every term can rewrite to NF.
Canonicity: every term rewrites into canonical form.
Then it leads to an intuition where if canonicity holds, then we get ...
3
votes
0answers
53 views
Semantics of “write-once” variables for complex data structures
Question
My use case for what is described below is not a language or compiler implementation, but finding a reasonable semantics for this feature in a an abstract calculus.
Ideally, you give me a ...
4
votes
1answer
367 views
Why do we need a separate notation for П-types?
Main
I am confused about the motivation behind the need for a separate notation for П-types, that you can find in type systems from λ2 on. The answer usually goes like so - think about how one can ...
1
vote
0answers
92 views
How do type classes make ad-hoc polymorphism less ad hoc?
The title of the paper that introduced type classes is "How to make ad-hoc polymorphism less ad hoc".
It seems the type classes approach is being compared to how OOP does ad-hoc polymorphism....
3
votes
0answers
92 views
(Co)-monads and terminating implementations
The bounty above should read 'I would like to know whether the example I discuss is a com-monad and why (why not).'
Suppose we set $\mathbb{M} \alpha := r \to \alpha$, where $r$ is some fixed type, ...
3
votes
1answer
256 views
The meaning and relevance of the locution ''no terminating implementation'' in type theory
In the context of a discussion of Haskell https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, I was told that
There is no terminating ...
2
votes
0answers
47 views
Difference between the logic and the type system of a proof assistant?
In Comparing Mathematical Provers (section 4.1), Wiedijk classifies logics and type systems of different proof assistants? I do not see what he means by type system of the assistant. He only says:
A ...
1
vote
2answers
87 views
How to express a type that represents an associative array whose keys determine the type of the value?
I'm fairly new to type systems and theory, so I would appreciate some guidance in a problem that sparked my interest.
I would like to understand what type system features are required so a compiler ...
