Maybe if I keep rewriting this document I will eventually stumble on what I want.
Goals:
- Support for programming environment with ever-increasing social vocabulary (i.e. 'helper' functions become global vocab words).
- "Type system" whose primary purpose is to document the meanings/usages of words.
The way I have been picturing (2) is by allowing types to be fabricated into existence without a formal (or representational) definition. For example, if we wanted to talk about primes as a type, we could, but we wouldn't have to describe to the computer what it means to be prime. It is human communication. So:
-- `inverse p n` finds the multiplicative inverse of n mod p.
inverse : Prime -> Nat -> Nat
more accurate:
inverse : (p : Prime) -> Z p -> Z p
even more accurate:
inverse : (p : Prime) -> Nonzero (Z p) -> Nonzero (Z p)
Something like that. Let's stick with the first one though.
The idea, then, is that Prime is not just a synonym for Nat. So if you have:
readNat : IO Nat
main = do
n <- readNat
m <- readNat
print $ inverse n m
You would get a type error (warning?) saying that n is not known to be Prime. Then you write some documentation
where
[n : Prime] because we are trusting the user to enter a prime
explaining the cast. But I think of it more as an assumption. So we can have n : Nat and n : Prime at the same time. But it is not looking so much like types now as "floating propositions".
The idea is to get the expressive modeling power of a dependently typed language without the burden of writing proofs. Instead we can write our proofs in English and the computer will just trust us. For the feel of the project, I see no need to support formal proofs at all (though it may help for automated proving, which I suspect will be necessary to some extent).
The hard part is determining how to handle relationships between propositions. For example, we want to encode the "common knowledge"
if [Prime p] then [Nat p]
but how/where is that stated, how does the checker know when to use it? It should go without saying; writing "I can add one to this prime because all primes are naturals" in the documentation is a waste of time. We could define a prime as a subtype of natural, but that is less modular than it could be (what if we defined it as a subtype of integer, and only later was the concept of natural introduced). Indeed, I am trying to move away from the constructive tradition of definition, toward a relational one.