Questions tagged [type-theory]

In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics.

type-theory
26 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
11 votes
0 answers
768 views

Encoding universal types in terms of existential types?

In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding ...
Agnishom Chattopadhyay's user avatar
11 votes
0 answers
486 views

In Idris, why do interface parameters have to be type or data constructors?

To get some practice with Idris, I've been trying to represent various basic algebraic structures as interfaces. The way I thought of organizing things at first was to make the parameters of a given ...
greatBigDot's user avatar
6 votes
0 answers
233 views

The world is not enough

I'm still trying to embed Observational Type Theory in itself and the whole thing into Agda. Currently I have the following hierarchy of universes: Prop : Type 0 : Type 1 : ... (∀ α -> Type α) : ...
effectfully's user avatar
  • 12.6k
5 votes
0 answers
148 views

Representing a fixpoint in a head-normal lambda calculus AST

Consider the following normalized term representation, obtained during type checking: data Normal a = Neutral (Neutral a) | Type | Pi (Normal a) (Normal (Maybe a)) | Abstract (Normal (Maybe a)...
jmegaffin's user avatar
  • 1,162
4 votes
1 answer
235 views

Beyond type theory

There has been much fuss about dynamically vs. statically typed languages. To my eye, however, while statically typed languages enable the compiler (or interpreter) to know a bit more about your ...
Rex Kerr's user avatar
  • 167k
3 votes
0 answers
333 views

In intuitionistic type theory, can any proof written in CoC be rewritten in system λP2? Or, does CoC = λP2?

(This question is under a permanent bounty of 1000 points, once proven/refuted, it will be retrospectively set up and awarded) (Possible duplicate: https://math.stackexchange.com/questions/4232108/%ce%...
tribbloid's user avatar
  • 3,946
3 votes
0 answers
1k views

How to pass a value of type `Union[bytes, str]` to function taking `AnyStr`

Suppose I have a couple of functions: from typing import Union, AnyStr def f(x: Union[bytes, str]): return g(x) def g(x: AnyStr): return x Running mypy on this causes an error :3: error: Value of ...
Teymour's user avatar
  • 1,949
3 votes
0 answers
185 views

How can linear-types replace monads?

I was doing some research into linear types and came across this comment on HN. Specifically, it says that in (Clean, ATS, etc ...), linear types are used to encode side-effects, as an ...
kuwze's user avatar
  • 411
3 votes
0 answers
184 views

F-bounded existential quantification

I came across the existential quantification for F-bounded types while trying to understand scala's type system. Let A be a type trait A[F <: A[F]] { self: F => } where F is the F-bounded ...
Björn's user avatar
  • 56
2 votes
0 answers
44 views

Type of union of disjunct functions?

Given two functions: f :: EvenInteger -> {0} g :: OddInteger -> {1} consider the function h = (x :: Integer) => { if(x is even)return f(x); return g(x); } What the smallest type T ...
Adam's user avatar
  • 1,352
2 votes
1 answer
249 views

How did the terms "leftmost" and "rightmost" (referring to generics) get their meaning?

Reading Angelika Langer's superb Generics FAQ, I'm finally starting to really grok some of the more subtle points of generics. But I'm still hungup on some of the jargon. My layman's understanding of ...
deduper's user avatar
  • 1,954
1 vote
0 answers
205 views

Scala variance positions - theory behind it?

Scala has notion of "variance position" and fancy rules around it, especially when variance is combined with method type bounds. Rules ensure type safety, one can read them in Scala lang ...
Max's user avatar
  • 1,795
1 vote
0 answers
78 views

NLTK.sem.logic cannot infer logical types of functions given types of argument and result, why?

I am working with NLTK.logic.sem to handle the logical structure of sentences. I also use NLTK to handle inferring the logical types of expressions. The NLTK book has an example of when it cannot ...
L. Suurmeijer's user avatar
1 vote
1 answer
28 views

Accessing Mapped Type where Values Cannot be Intersected, Handler Pattern

I'm not sure if the title accurately describes my issue, but here is the code I'm working with: const EnumValues = ["a", "b", "c"] as const; type Enum = typeof EnumValues[...
Enrico Borba's user avatar
  • 2,007
1 vote
1 answer
104 views

What is the full space of parametrically polymorphic functions (not ad hoc polymorphic) operations in programming languages?

On page 349 paragraph 5 of A Theory of Type Polymorphism in Programming, Milner says, For us, the polymorphism present in a program is a natural outgrowth of the primitive polymorphic operators which ...
Conor Quinn's user avatar
1 vote
0 answers
677 views

Lean : Proof that \ not p \to (p \ to q) or similar false \to p

I am new at lean - prover and I am trying to solve the examples on the online tutorial. I am stuck at this example and I need to prove that "false implies q" or something like that. My code is : ...
Georgios Papanikolaou's user avatar
1 vote
0 answers
36 views

Type System attributes : Developing intuition and Addressing Misconceptions

A type system is a set of rules used to provide additional layer of information about entities in a program, so that the runtime, or the compiler, or any other piece of machinery, knows what to do ...
Gabriele Scarlatti's user avatar
1 vote
0 answers
292 views

Implementation of Transitivity of Equality in Agda (HoTT)

After hours of trying different versions of it, I give up. I just want to typecheck a proof of the transitivity of equality as stated in the HoTT-Book. I'm new to Agda so it might be just a small flaw ...
Greg P.'s user avatar
  • 193
1 vote
0 answers
147 views

Interpretation of Partial Functions from Z to Isabelle/HOL

I am trying to write a predicate such that, "if a certain constant is true"(in this case if 'sec=ok') then the predicate will evaluate to False, because I've written an expression in the consequent of ...
user3896306's user avatar
1 vote
1 answer
180 views

Decidability of bi-cartesian closed categories

Is the decision problem for the free bi-cartesian closed category (BCCC) decidable? Equivalently, is equality decidable for the simply-typed lambda calculus extended with strong n-ary products and ...
Ryan Wisnesky's user avatar
0 votes
0 answers
18 views

Parity of nested function type and recursive call

I'm working on recursive types (involving only functions; a -> b). For each type with one self-reference I can tell whether it's possible to write a function that calls itself with that type. For ...
pollatron's user avatar
0 votes
0 answers
67 views

Hindley-Milner - conditional Substitutions?

I have been trying to build a type system with the Hindley-Milner Algorithm and ran into the following challenge and was curious if there are any resources or papers out there I can take a look at. ...
databasechaser's user avatar
0 votes
0 answers
38 views

How to type a compiler?

Take two abstract machines and two instructions the semantics of which is encoded in the following fictional (functional) language: class incr; // preserves @code, increments @pc, increments @x fn ...
Adam's user avatar
  • 1,352
0 votes
0 answers
84 views

Are types that are neither inductive nor coinductive needed for writing real world programs?

Or it's just sometimes it's too hard to prove a type is a coinductive one? I'm talking about a programming language that is total which means it's not Turing complete, and recursion are all ...
盛安安's user avatar
  • 1,149
0 votes
1 answer
98 views

Algorithm W and monomorphic type coercion

I'm trying to write my own type inference algorithm for a toy language, but I'm running into a wall - I think algorithm W can only be used for excessively general types. Here are the expressions: ...
Athan Clark's user avatar
  • 3,896