[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Axiom musings ... runtime computation of first-class dependent types

From: Martin Baker
Subject: Re: Axiom musings ... runtime computation of first-class dependent types
Date: Sun, 29 May 2022 17:44:24 +0100
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101 Thunderbird/91.9.0


In this series of videos Robert Harper gives an provocative take on these subjects:

At about 37 min into this video he says: "what is true has unbounded quantifier complexity whereas any formalism is always relentlessly recursively innumerable" - Gödels theorem.

"there is a distinction between proof and truth"
(by formalism here I think he means formal logic?)

It looks to be like the programming style he is putting forward is dynamic typing? I cant find it now, in these videos, but I think he might have suggested that this style of programming is required to model all of mathematics (be foundational)? Even cubical type theory might not be foundational?

Do you think that dynamic types and/or the sort of self modifying programs you are suggesting are necessary to model all of mathematics?

These videos are 4 years old, do you know if this research has come to any conclusions on these issues?


On 29/05/2022 08:50, Tim Daly wrote:
Well, SANE is certainly turning into a journey.

When we look at the idea of first-class dependent types
as implemented in languages like Agda and Idris we find
what I call "peano types". For example, Fin is a type
of "finite numbers", usually defined as

data Fin : Nat -> Type where
   FZ : Fin (S n)             -- the base case
   FS : Fin n -> Fin (S n)    -- the recursive case

Fin 7 describes 7 numbers 0..6

This construction is popular because the compiler can
compute that the type construct is total. Thus the
type construct is its own proof.

A dependent type allows computation to occur during
its construction. The canonical example is defining
a list of length m, which depends on the value of m.
Another list of length n is a separate type. An
append function of these lists computes a new typed
list of length (m + n).

The current approach, Agda, Idris, etc., is "bottom up"
where restrictions are placed which will allow proofs
in all contexts.

There are excellent reasons for such carefully
styled dependent types.

Reading the literature you come across the famous
Dan Friedman admonition "Recursion is not allowed",
usually in reference to his Pie language [0]. While
Pie does not allow it, he admits 2 kinds of recursion
(pp 358-359).

The general case of first-class dependent types I'm
considering is capable of much broader and more
ill-founded behavior. This is deliberate because some
of the mathematics in Axiom can only be proven correct
under limited cases. These cases have to be constructed
"on the fly" from more general dependent type definitions.

For example, a type might not be total in general but
it may be possible to compute a bounded version of the
type when used in context. This can only be decided at
run time with the given parameters in the given context.
In general, this means computing that "in this context
with these bindings the result can be proven".

This general case occurs because a SANE type G is able to
invoke all of lisp with an environment that contains the
type G under construction as well as its environment
which contains the program. This allows the type G to self
reference and self modify based on context.

The general type G:List(G,REPL) in a context of a statement
M:G := (append '(1 2 3) '(4 5 6 7)) as effectively typed

The SANE type G is neither sound nor complete but List(7) is.
The game is to construct a contextually dependent type and
the associated proof "on the fly".

An intuitive Gedankenexperiment is defining an arm for a
general robot. One could have a 2 arm robot defined as
Robot : TwoArm(Robot,Repl).

The problem, based on context, might generate each of the
two arms separately, one with 7 degress of freedom to
reach the whole of the workspace (in context) and a second
4 degree robot that can position and hold a part in the
reach of the first arm. The same TwoArm type might resolve
to a different configuration in a different context.

Self-reference is already a metamathematical problem
(witness Godel's proof). Self-modification is, as Monty
Python famously says, "right out". One might argue with
Godel but contradicting Python is heresy.

The SANE game is to create the general case of first-class
dependent types with such abilities and then find certain
restrictions as necessary to try to construct the proof
in a given context. This SOUNDs COMPLETEly crazy, of course.

One has to construct a lisp program "on the fly" in the
dependent type context, prove it correct, and return the
new type with the type-program and proof. Values, during the
run time computation may have to be dynamically substituted
in the type-program, re-running the proof with those values.

At best this ranges from the nearly impossible to horribly
inefficient. We all know this can never work.

This seems necessary as Axiom's computer algebra algorithms
were never developed with proof in mind. It seems necessary
to start "from the top" and work downward to the instance
of existing code, adding restrictive assumptions as needed.

The moral of the story is "Never give a lisper a REPL".

There are some who call me ... Tim [1]

Amusing historical note: Code linters were discovered during an
omphaloskepsis session.

[0] Friedman, Daniel P. and Christiansen, David Thrane
"The Little Typer", MIT Press (2018) ISBN 978-0-262-53643-1

[1] <>

reply via email to

[Prev in Thread] Current Thread [Next in Thread]