[HN Gopher] Typechecking is undecideable when 'type' is a type (...
___________________________________________________________________
Typechecking is undecideable when 'type' is a type (1989) [pdf]
Author : birdculture
Score : 44 points
Date : 2025-11-18 11:33 UTC (5 days ago)
(HTM) web link (dspace.mit.edu)
(TXT) w3m dump (dspace.mit.edu)
| IshKebab wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| Ah is that what Lean does with its type universes?
| cjfd wrote:
| Yes, it is.
| SkySkimmer wrote:
| >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 wrote:
| 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 wrote:
| 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 wrote:
| It's "kind" of over your head, eh?
| TazeTSchnitzel wrote:
| This must be why kinds (types of types) in Haskell are a separate
| and less powerful thing than ordinary types?
| amelius wrote:
| I suspect not, because in that case Type is not a Type itself,
| but a Kind.
| alcidesfonseca wrote:
| 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 wrote:
| With respect to Lean/Rocq, that's true, with the subtle
| difference that Rocq universes are cumulative and Lean's are
| not.
| marcosdumay wrote:
| Access is currently forbidden.
| jonasmalaco wrote:
| Currently blocked in Brazil, 49/50 pings return 403/forbidden:
| https://globalping.io/?measurement=2acUvndlTojar3qy80001zLzv
| burakemir wrote:
| 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 wrote:
| "A Polymorphic l-calculus with Type:Type"
| randomNumber7 wrote:
| I will implement that in my pension if no one else does it in
| the next 30 years.
| captaincrowbar wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| Hmm okay. That makes perfect sense to me, although it still
| isn't something I'd get from the language they used.
| tomp wrote:
| 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/
___________________________________________________________________
(page generated 2025-11-23 23:01 UTC)