Typechecking is undecideable when 'type' is a type (1989) [pdf]

https://dspace.mit.edu/bitstream/handle/1721.1/149366/MIT-LCS-TR-458.pdf

48•birdculture•2mo ago

Comments

IshKebab•2mo ago

I haven't read this, and I'm not a type theorist so this is kind of over my head, but my understanding is that you can have decidable dependent types if you add some constraints - see Liquid types (terrible name).

https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li...

cjfd•2mo ago

One way that is very common to have decidable dependent types and avoid the paradox is to have a type hierarchy. I.e, there is not just one star but a countable series of them *_1, *_2, *_3, .... and the rule then becomes that *_i is of type *_(i+1) and that if in forall A, B A is of type *_i and B is of type *_j, forall A, B is of type type *_(max(i, j) + 1).

khaledh•2mo ago

I'm no expert myself, but is this the same as Russell's type hierarchy theory? This is from a quick Google AI search answer:

    Bertrand Russell developed type theory to avoid the paradoxes, like his own, that arose from naive set theory, which arose from the unrestricted use of predicates and collections. His solution, outlined in the 1908 article "Mathematical logic as based on the theory of types" and later expanded in Principia Mathematica (1910–1913), created a hierarchy of types to prevent self-referential paradoxes by ensuring that an entity could not be defined in terms of itself. He proposed a system where variables have specific types, and entities of a given type can only be built from entities of a lower type.

cjfd•2mo ago

I don't know that much about PM but I from what I read I have the impression that for the purposes of paradox avoidance it is exactly the same mechanism but that PM in the end is quite different and the lowest universe of PM is much smaller than than that of practical type theories.

IshKebab•2mo ago

Ah is that what Lean does with its type universes?

cjfd•2mo ago

Yes, it is.

SkySkimmer•2mo ago

>if in forall A, B A is of type _i and B is of type _j, forall A, B is of type type *_(max(i, j) + 1).

Minor correction: no +1 in forall

anon291•2mo ago

This is correct but just delays the problem. It is still impossible to type level-generic functions (i.e. functions that work for all type levels).

The basic fundamental reality that no type theory has offered is an ability to type everything

alcidesfonseca•2mo ago

Liquid Types are more limited than "full dependent types" like Lean, Rocq, Agda or Idris. In Liquid Types you can refine your base types (Int, Bool), but you cannot refine all types. For instance, you cannot refine the function (a:Int | a > 0) -> {x:Int | x > a}. Functions are types, but are not refinable.

These restrictions make it possible to send the sub typing check to an SMT solver, and get the result in a reasonable amount of time.

blurbleblurble•2mo ago

It's "kind" of over your head, eh?

TazeTSchnitzel•2mo ago

This must be why kinds (types of types) in Haskell are a separate and less powerful thing than ordinary types?

amelius•2mo ago

I suspect not, because in that case Type is not a Type itself, but a Kind.

alcidesfonseca•2mo ago

I believe it to be historically true, but Dependent Haskell might change this (https://ghc.serokell.io/dh see unification of types and kinds).

In Lean (and I believe Rocq as well), the Type of Int is Type 0, the type of Type 0 is Type 1, and so on (called universes).

They all come from this restriction.

aureianimus•2mo ago

With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.

marcosdumay•2mo ago

Access is currently forbidden.

jonasmalaco•2mo ago

Currently blocked in Brazil, 49/50 pings return 403/forbidden: https://globalping.io/?measurement=2acUvndlTojar3qy80001zLzv

burakemir•2mo ago

I remember a Luca Cardelli paper that explores a language with "type:type" and it contains a sentence roughly expressing: "even if the type system is not satisfying as a logic, it offers interesting possibilities for programming"

burakemir•2mo ago

"A Polymorphic λ-calculus with Type:Type"

randomNumber7•2mo ago

I will implement that in my pension if no one else does it in the next 30 years.

captaincrowbar•2mo ago

This feels like a restatement of the trivially obvious observation that, if your type system is Turing complete, you're going to run into the halting problem.

acjohnson55•2mo ago

I'm not sure it is exactly the same. But even if so, someone needed to do the work to prove it. It's also worth noting that proving the undecidability of the halting problem is one of the reasons Turing is so celebrated in the first place.

wavemode•2mo ago

I don't think that's quite it. In many statically-typed languages that we would typically refer to as having "Turing-complete type systems", types cannot be manipulated at runtime, and thus Type is not really a type in the same way that e.g. int or float are types.

It's sort of like having two languages in one. There is a first, interpreted language which manipulates Types and code and produces a program, and then a second language which is the program itself that ultimately gets typechecked and compiled. Typechecking in this case is not (necessarily) undecidable.

This paper is moreso about dependently-typed languages, where the type of one term can depend on the runtime value of another term.

saghm•2mo ago

I'm probably at the level of "moderately skilled amateur" when it comes to type theory (I took courses in college about compilers and the math behind type theory like Hoare logic), but I got confused by the second sentence:

> A function has a dependent type when the type of its result depends upon the value of its argument

Pretty straightforward, and something I'm familiar with.

> The type of all types is the type of every type, including itself.

I...don't know what this means. It's unclear to me how to understand the meaning of "the type of every type", since I don't have an intuition of how to "combine" all of those types into something that I can reason about. My first instinct would be that it's saying it's a set, but if it contains itself, doesn't that run into Russel's paradox (unless they're assuming some specific set of axioms around set construction to solve this, which seems strange to leave implicit)?

Am I missing something obvious, or is it kind of unclear what they're talking about here? Maybe my confusion is that I feel like the difference between "all" and "every" is ambiguous, so I don't know how to read this as circular other than logically grouping "all types" into one thing and "every type" into a group of separate things, only I don't know what that group even is.

wavemode•2mo ago

So, let's say you have a term: 5

5 is a value of the type Integer.

What the paper is saying, is that we can go two steps further - Integer itself is a value of the type Type, and Type itself is also a value of the type Type.

The paper uses * as a symbol (and "type of all types" as a description) designating the type Type.

saghm•2mo ago

Hmm okay. That makes perfect sense to me, although it still isn't something I'd get from the language they used.

1718627440•2mo ago

It is easy to understand in practice. For example in Python:

    >>> type(5)
    <class 'int'>

    >>> type(type(5))
    <class 'type'>

    >>> type(type(type(5)))
    <class 'type'>

tomp•2mo ago

Yeah, it's very easy to get into a situation of "type is a subtype of a larger version of itself" which obviously grows without bounds.

But the solution is trivial - basically the same as the old mathematical issue "set vs class": only small types are types, large types aren't. Which types are "small"? Well, precisely those, that don't contain abstract types.

See this brilliant paper for a longer treatise (the above is the essential summary): 1ML by Andreas Rossberg

https://people.mpi-sws.org/~rossberg/1ml/

OpenClaw Is Changing My Life

Everything you need to know about lasers in one photo

SCOTUS to decide if 1988 video tape privacy law applies to internet uses

Epstein files reveal deeper ties to scientists than previously known

Red teamers arrested conducting a penetration test

Show HN: Open-source AI powered Kubernetes IDE

Show HN: Lucid – Use LLM hallucination to generate verified software specs

AI Doesn't Write Every Framework Equally Well

Aisbf – an intelligent routing proxy for OpenAI compatible clients

Let's handle 1M requests per second

OpenClaw Partners with VirusTotal for Skill Security

Goal: Ship 1M Lines of Code Daily

Show HN: Codex-mem, 90% fewer tokens for Codex

FastLangML: FastLangML:Context‑aware lang detector for short conversational text

LineageOS 23.2

Crypto Deposit Frauds

Substack makes money from hosting Nazi newsletters

Framing an LLM as a safety researcher changes its language, not its judgement

Are there anyone interested about a creator economy startup

Show HN: Skill Lab – CLI tool for testing and quality scoring agent skills

2003: What is Google's Ultimate Goal? [video]

Roger Ebert Reviews "The Shawshank Redemption"

Busy Months in KDE Linux

Zram as Swap

Green’s Dictionary of Slang - Five hundred years of the vulgar tongue

Nvidia CEO Says AI Capital Spending Is Appropriate, Sustainable

Show HN: StyloShare – privacy-first anonymous file sharing with zero sign-up

Part 1 the Persistent Vault Issue: Your Encryption Strategy Has a Shelf Life

Show HN: Teleop_xr – Modular WebXR solution for bimanual robot teleoperation

The Highest Exam: How the Gaokao Shapes China

OpenClaw Is Changing My Life

Everything you need to know about lasers in one photo

SCOTUS to decide if 1988 video tape privacy law applies to internet uses

Epstein files reveal deeper ties to scientists than previously known

Red teamers arrested conducting a penetration test

Show HN: Open-source AI powered Kubernetes IDE

Show HN: Lucid – Use LLM hallucination to generate verified software specs

AI Doesn't Write Every Framework Equally Well

Aisbf – an intelligent routing proxy for OpenAI compatible clients

Let's handle 1M requests per second

OpenClaw Partners with VirusTotal for Skill Security

Goal: Ship 1M Lines of Code Daily

Show HN: Codex-mem, 90% fewer tokens for Codex

FastLangML: FastLangML:Context‑aware lang detector for short conversational text

LineageOS 23.2

Crypto Deposit Frauds

Substack makes money from hosting Nazi newsletters

Framing an LLM as a safety researcher changes its language, not its judgement

Are there anyone interested about a creator economy startup

Show HN: Skill Lab – CLI tool for testing and quality scoring agent skills

2003: What is Google's Ultimate Goal? [video]

Roger Ebert Reviews "The Shawshank Redemption"

Busy Months in KDE Linux

Zram as Swap

Green’s Dictionary of Slang - Five hundred years of the vulgar tongue

Nvidia CEO Says AI Capital Spending Is Appropriate, Sustainable

Show HN: StyloShare – privacy-first anonymous file sharing with zero sign-up

Part 1 the Persistent Vault Issue: Your Encryption Strategy Has a Shelf Life

Show HN: Teleop_xr – Modular WebXR solution for bimanual robot teleoperation

The Highest Exam: How the Gaokao Shapes China

Typechecking is undecideable when 'type' is a type (1989) [pdf]

Comments