This page presents some speculative ideas/proposals (from Ben Goertzel) regarding how to utilize the Agda programming language as a framework for
- coding Atomese
- type-checking complex Atomese
- eventually, proving correctness or other properties of complex Atomese
The ideas here could eventually also lead to use of OpenCog to help with complex type checking (aka automated theorem proving) within Adga, thus leading to a hybrid OpenCog-Agda theorem-proving framework. But the comments here will focus on earlier/simpler steps than this.
(NOTE: I believe all of the ideas outlined below below would work in Agda right now. However, some of it may involve some inelegance in the setup of Agda definitions. From what I can tell, these inelegances could be fixed by relatively minor hacking within the (Haskell) implementation of Agda; but of course, any such hacking is only "minor" for someone who already understands the Haskell implementation of Agda...)
Atoms and Atom types in Agda
OpenCog Atom types can be constructed straightforwardly within Agda.
Further, this can be done in a way that abstracts away from efficiency-oriented infelicities/asymmetrics in the actual Atomspace implementation. For instance, the symmetry between Atom types and predicates can be reflected in the Agda implementation of both (so that e.g. "InheritanceLink" and "eat" can be represented basically the same way in Agda, alongside the sometimes-useful additional knowledge that "InheritanceLink" is considered a Link type and "eat" is considered a PredicateNode).
Further comments will be given on this below in the context of the proposed "Atomize" method.
(examples to be added here as time permits)
Type signatures in Agda
Type signatures for OpenCog Predicates and Schema also can be constructed straightforwardly in Agda.
(examples to be added here as time permits)
Specific Atoms in Agda
Specific Atom content, including DefinedSchemaNodes, can be built straightforwardly in Agda.
(examples to be added here as time permits)
Agda for OpenCog type checking
Given the above, a "simple" use of Agda would be: Create a module of Atom types in Agda, and check that it's consistent. Then, when you create a bunch of specific Atoms in Agda, you can check that all their signatures have been constructed consistently.
Agda could also potentially be used for type checking OpenCog Atom-sets not created within Agda (i.e. Atoms created via Scheme or python, or created automatically via OpenCog AI methods). To enable this, the mapping from OpenCog types to Agda types could also be done in the opposite direction. Given a mapping from OpenCog type signatures to Agda types, we could then use Agda's type-checker to check consistency of a set of OpenCog types. This might be slow; on the other hand, for almost all OpenCog cases it might be adequately fast due to the simplicity of the current OpenCog type signatures from a type-theoretic perspective.
Note that the current C++ implementation already has a type checker; it is implemented as a utility that is used in a variety of subsystems to ensure coherent operation. For example, it is is central to the implementation of the filtering done by MapLink.
For the above to be directly useful in OpenCog, we would need to write an Agda "Atomize" method, which takes a bunch of Atom types and specific Atoms (which are constructed within Agda in a parallel way), and actually loads them into the Atomspace. This would use the existing Haskell interface to the Atomspace, via Adga's ability to invoke Haskell methods.
The implementation of the Atomize method would be moderately complicated with a lot of special cases, as it would have to account for all the ways in which the Atomspace implementation embodies efficiency-oriented asymmetries whereas the Agda versions of Atoms are more elegant and more reflective of the underlying mathematical structure. Operationally, Atomize would take a bunch of Agda code and generate a bunch of Haskell code, and then load this Haskell code into a specified Atomspace.
Abstracting away from Atomspace particulars
The Atomize method could be used to encapsulate Atomspace implementation particulars, allowing the Agda-Atomese itself to avoid getting tangled in these.
- InheritanceLink ( ConceptNode "cat", ConceptNode "animal")
- EvaluationLink (PredicateNode "eat" (ConceptNode "Cat", ConceptNode "mouse"))
- ConceptNode "Cat" <.8>
are all basically just ternary relations .
- (InheritanceLink, ConceptNode "cat", ConceptNode "animal")
- (PredicateNode "eat", ConceptNode "cat", ConceptNode "mouse")
- (truth value strength, ConceptNode "cat", .8 )
but in the current Atomspace they are represented in quite different ways, for a complex mix of historical and efficiency reasons
In an Agda Atomese as proposed here, these would all be implemented symmetrically, and then the Atomize method would do the Atomspace-implementation-specific work to map everything into Atoms in the right way
Atomize would need to be Agda rather than Haskell because not all the Atom types created in Agda-Atomese would necessarily correspond to Haskell types, so the Atomize method would translate the Agda types into the single Haskell "Atom" type with appropriate associated metadata...
Then changes in Atomspace representation/implementation would require changes to the guts of the Atomize method, but not changes to other Agda-Atomese code...
Mapping Generic Agda into Atomese?
Here is a more advanced usage, that would be interesting to explore after the above stuff all works.
Inside the definition of an Agda-Atomese DefinedSchemaNode, one could allow plain old Agda code, i.e. arbitrary Agda constructs, not just types inheriting from Atom. One could then extend Atomize to transform an arbitrary Agda construct into Atoms, and load such DefinedSchemaNodes into OpenCog.
The point here would be
- to use Agda as syntactic sugar for Atomese, i.e. this would let one use the native Agda syntax to construct Atomese.
- to open the door for using OpenCog to help Agda do its own internal stuff (e.g. to use AI to optimize complex type checking)
Since the Agda syntax is relatively minimal and wholly functional, without a lot of bells and whistles, this enhanced Atomize would not need to be *insanely* complicated, though it would certainly be a non-trivial piece of Agda coding.
Probabilistic Programming over Adga?
Note that, combined with the SampleLink proposal for OpenCog, this would enable an interesting sort of probabilistic programming over Agda ... using OpenCog to fuse probabilistic programming and dependent type theory in a unique, fascinating and AGI-friendly way.
Agda + PLN semantics
There seems to be a nice nice synergy btw Agda's constructive math foundations and PLN's observational semantics...
By constructing Atomese in Agda, and type-checking it, one validates that the Atoms one is constructing all have consistent types.... Putting this together with the "observational semantics" of OpenCog Atom types like InheritanceLink, PredicateLink, MemberLink etc. etc. -- this means: one validates that the Atoms one is constructing can all have their truth values updated based on some observations. The constructivist foundation of math underlying Agda's type theory, matches naturally with the observational semantics underlying PLN -- so that one is only building stuff in the Atomspace that can have its truth value updated via observations, via some specific series of inferences...
Tweaking Agda later on?
After playing with steps 1-4 above for complex cases, we may come up with ideas for tweaking Agda syntax to make coding Atomese-in-Agda more concise and readable. Given the early stage of development of the Agda language, getting syntax enhancements adopted into the main stream of Agda versions is not an outrageous possibility. (If we did start using Agda for OpenCog, we would be the only "practical" users of the language; at the moment it seems to be used only for research into automated theorem-proving.)
Also, as noted at the start, the proposed use of Agda may highlight some minor inelegancies in the current Agda front-end; e.g. the minor hacks needed to implement inheritance hierarchies as noted here:
None of these seem a big problem at the moment, but they indicate areas where OpenCog utilization might help drive generically useful Agda improvements.
Can OpenCog AI help Agda?
It seems likely that to make type checking in dependent type theory scalably functional, some advanced AGI will be needed.
This could be done, perhaps, by completing the loop and using OpenCog to help guide Agda's internal type-checking. This would obviously rely on the "Mapping generic Agda into Atomese" step mentioned above, but would also need a lot more -- e.g. it would require effective use of PLN and pattern mining and ECAN and other OpenCog AI methods for theorem-proving. This is speculated about in the "Engineering General Intelligence vol. 2" book but no concrete work has been done on this so far. Hybridization of OpenCog with Agda presents one promising direction for fleshing out and pursuing the vague speculations given there.
This is an important fundamental direction in terms of enabling advanced AGI functionality such as goal-directed intelligent self-modification.