Axiom musings ... runtime computation of first-class dependent types
Tim Daly <[email protected]> Sun, 29 May 2022 03:50:42 -0400
| Newsgroups | gmane.comp.mathematics.axiom.devel |
|---|---|
| Message-ID | <CAJn5L=JaN52VG_6HSRrRPmUacJUARbJEA1+ukWp6Xr05XZ0KVA@mail.gmail.com> |
--0000000000008edd9705e021ccab Content-Type: text/plain; charset="UTF-8" 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 M:List(7). 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] https://www.youtube.com/watch?v=co3ygE6H7PU --0000000000008edd9705e021ccab Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr">Well, SANE is certainly turning into a journey.<br><br>Whe= n we look at the idea of first-class dependent types<br>as implemented in l= anguages like Agda and Idris we find<br>what I call "peano types"= . For example, Fin is a type<br>of "finite numbers", usually defi= ned as<br><br>data Fin : Nat -> Type where<br>=C2=A0 FZ : Fin (S n) =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 -- the base case<br>=C2=A0 FS : Fin = n -> Fin (S n) =C2=A0 =C2=A0-- the recursive case<br><br>Fin 7 describes= 7 numbers 0..6<br><br>This construction is popular because the compiler ca= n<br>compute that the type construct is total. Thus the<br>type construct i= s its own proof.<br><br>A dependent type allows computation to occur during= <br>its construction. The canonical example is defining<br>a list of length= m, which depends on the value of m.<br>Another list of length n is a separ= ate type. An<br>append function of these lists computes a new typed<br>list= of length (m + n).<br><br>The current approach, Agda, Idris, etc., is &quo= t;bottom up"<br>where restrictions are placed which will allow proofs<= br>in all contexts.<br><br>There are excellent reasons for such carefully<b= r>styled dependent types.<br><br>Reading the literature you come across the= famous<br>Dan Friedman admonition "Recursion is not allowed",<br= >usually in reference to his Pie language [0]. While<br>Pie does not allow = it, he admits 2 kinds of recursion<br>(pp 358-359).<br><br>The general case= of first-class dependent types I'm<br>considering is capable of much b= roader and more<br>ill-founded behavior. This is deliberate because some<br= >of the mathematics in Axiom can only be proven correct<br>under limited ca= ses. These cases have to be constructed<br>"on the fly" from more= general dependent type definitions.<br><br>For example, a type might not b= e total in general but<br>it may be possible to compute a bounded version o= f the<br>type when used in context. This can only be decided at<br>run time= with the given parameters in the given context.<br>In general, this means = computing that "in this context<br>with these bindings the result can = be proven".<br><br>This general case occurs because a SANE type G is a= ble to<br>invoke all of lisp with an environment that contains the<br>type = G under construction as well as its environment<br>which contains the progr= am. This allows the type G to self<br>reference and self modify based on co= ntext.<br><br>The general type G:List(G,REPL) in a context of a statement<b= r>M:G :=3D (append '(1 2 3) '(4 5 6 7)) as effectively typed<br>M:L= ist(7).<br><br>The SANE type G is neither sound nor complete but List(7) is= .<br>The game is to construct a contextually dependent type and<br>the asso= ciated proof "on the fly".<br><br>An intuitive Gedankenexperiment= is defining an arm for a<br>general robot. One could have a 2 arm robot de= fined as<br>Robot : TwoArm(Robot,Repl).<br><br>The problem, based on contex= t, might generate each of the<br>two arms separately, one with 7 degress of= freedom to<br>reach the whole of the workspace (in context) and a second<b= r>4 degree robot that can position and hold a part in the<br>reach of the f= irst arm. The same TwoArm type might resolve<br>to a different configuratio= n in a different context.<br><br>Self-reference is already a metamathematic= al problem<br>(witness Godel's proof). Self-modification is, as Monty<b= r>Python famously says, "right out". One might argue with<br>Gode= l but contradicting Python is heresy.<br><br>The SANE game is to create the= general case of first-class<br>dependent types with such abilities and the= n find certain<br>restrictions as necessary to try to construct the proof<b= r>in a given context. This SOUNDs COMPLETEly crazy, of course.<br><br>One h= as to construct a lisp program "on the fly" in the<br>dependent t= ype context, prove it correct, and return the<br>new type with the type-pro= gram and proof. Values, during the<br>run time computation may have to be d= ynamically substituted<br>in the type-program, re-running the proof with th= ose values.<br><br>At best this ranges from the nearly impossible to horrib= ly<br>inefficient. We all know this can never work.<br><br>This seems neces= sary as Axiom's computer algebra algorithms<br>were never developed wit= h proof in mind. It seems necessary<br>to start "from the top" an= d work downward to the instance<br>of existing code, adding restrictive ass= umptions as needed.<br><br>The moral of the story is "Never give a lis= per a REPL".<br><br><div>There are some who call me ... Tim [1]</div><= div><br></div><div><br></div><div><br></div><div><br></div><div>Amusing his= torical note: Code linters were discovered during an<br></div><div>omphalos= kepsis session.<br></div><br>[0] Friedman, Daniel P. and Christiansen, Davi= d Thrane<br>"The Little Typer", MIT Press (2018) ISBN 978-0-262-5= 3643-1<br><br>[1] <a href=3D"https://www.youtube.com/watch?v=3Dco3ygE6H7PU"= >https://www.youtube.com/watch?v=3Dco3ygE6H7PU</a><br></div> --0000000000008edd9705e021ccab--