For my Artificial Intelligence 2 class I have to do a tool review of some piece of software related to AI. While my thesis is in the field of Evolutionary Algorithms, my main interest is really in functional programming and the related theory (the lambda calculi, type theories, intuitionistic logic, and category theory) so I'm planning on doing a review of a theorem prover or assistant like agda. The relation to AI here is that such tools come out of the symbolic AI community historically.
While reading an introduction to Agda, I came across a sentence about the features of the language that made me literally laugh out loud. In addition to an amazing type system they mention that "Agda’s logical framework also provides record types and a countable sequence of larger universes Set = Set0 , Set1 , Set2 , . . ..".
Both record types and an infinite number of universes? What a language!
nice. Does that mean you could create a universe using data structures?
ReplyDeleteAs far as I'm concerned- yes. Yes it does.
ReplyDeleteTheir referring to the fact that when we talk about something having a type, like 3 is of type Integer, we must ask- what type is Integer? If it is of type Type, then what is the type of Type? If it is also Type we might end up with some self referential paradoxes, so lets make it of type Kind. And the type of Kind? And the type of the type of Kind? In Agda the type of types is Set and the type of Set is Set1, and the type of Set1 is Set2, and so on.
In Haskell this is treated differently- most types have type "*" (pronounced Kind) and type constructors (which are things like [] in c, a type that depends on another type- you never make an array, you can only make an array of *something*), have kinds like "* -> *" or "* -> * -> *". This means that on top of the polymorphic lambda calculus that Haskell is very similar to, there is a simply typed lambda calculus of kinds with only the constructor "->".
ReplyDelete