> I'm curious: how many people have actually written a program in
> Cayenne? How many people have written programs that made significant
> use of the dependent typing? Has anybody tried to teach a programming
> class using Cayenne?
I'll admit to not having yet written something in Cayenne, but I'm an
adamant supporter of adding dependant types to the language. I remember a
year ago, I was writing a small (trivial) program. One of the essential ways
I was structuring the program was with a function "apply" similar to
Lisp/scheme's apply. Needless to say, you can't express apply in Haskell
although you can in Cayenne. In the context of this problem, I could easily
get around this by restructuring my program, but this was obviously not
ideal. We should be able to express trivial functions like apply in the type
system.
> apply f (p:ps) = apply (f p) ps
> apply f [] = f
I wanted to express the type as something like:
> apply :: (a -> a -> ... -> a) [a] -> a
The stated domain of apply is much larger than its actual domain. I want its
domain to be:
a function whose arity is the length of the second parameter (a list).
It's clear that the precise domain of apply can only be expressed with a
function.
I would like to say that the type of the first parameter is applyType:
applyType a [] = a
applyType a (p:ps) = a -> applyType a ps
I presume the type of the applyType is then
applyType :: (a :: #) -> [a] -> #
with # being the type of all types.
Thus apply is of type
apply :: (applyType a l) (l :: [a]) -> a
Now there are a ton of problems with what I just stated.
1) The type of apply is somewhat ambiguous. The a passed to applyType is
free.
Assumption: free variables are universally quantified. This is consistent
with Haskell's current notation for typing.
2) This isn't valid Cayenne (I'll get to this later)
3) The type of applyType can be more specific.
Recall,
applyType :: (a :: #) -> [a] -> #
The final # is actually just function space.
How would we express the notion of a function space? Well, lets start with
the simpler problem of defining the n-function space (my vocabulary is
obviously falling apart at this point).
F :: (a :: #) Integer -> #
F a 0 = a
F a n = a -> (F a (n - 1))
We however want to generalize this... I'm not quite sure how to describe it,
but I'll do the following:
F a * = member (map (F a) [0..]) // member [a] a -> Bool
so applyType is then
applyType :: (a :: #) -> [a] -> (F a *)
and applyType can be defined more succinctly:
applyType a l = F a (length l)
and since the recursion has been eliminated from applyType, you can eschew
applyType altogether and type apply thusly:
apply :: (F a (length l)) (l :: [a]) -> a
This is satisfactory, but a reasonable request is to make the *range* of
apply even more general. Since apply's first parameter is a curried
function, it seems to me that there's no reason why the range of apply can't
also be a function. That is,
apply should return a value of type a iff the length of its second parameter
equals the arity of its first. Otherwise, the length of the second must be
less than the arity of the first, in which case apply should return a
function whose arity is the difference of the arity first parameter and the
length of the second.
Example:
apply (+) [1] == \x -> 1 + x
so one now expresses the type of apply thusly:
apply :: (F a *) (l :: [a]) -> (F a *).
This isn't completely satisfactory, since the first parameter of apply and
the range are now too general.
To make them specific, I define the following:
arity :: (F a *) -> Int
arity (a -> as) = 1 + (arity as)
arity a = 0
Fr a min max = member (map (F a) [min..max])
so apply is now typed
apply :: (f :: (Fr a [(length l)..])) (l :: [a])
-> (F a ((arity f) - (length l)))
whew.
Now I must warn you that I'ven't checked anything at all, so it is highly
probable that there are errors. Like, I'm introducing things like pattern
matching on the function type constructor (->). I'm not sure if this is
valid.
Some questions for Lennart (and those more knowledgeable than I):
[1] What type can Cayenne infer for apply just given apply's definition?
[2] I know my last type for apply is invalid cayenne due to the order of
parameters and such, but if it's massaged a little bit: can Cayenne type
check it?
Foremost is that dependant types allow us to type more things than before.
The example I've shown demonstrates that even a simple thing like apply
needs them. One might infer, then, that there are possibly many simple and
perhaps common things which require this sort of type system.
It is also clear, however, that dependant types are no trivial thing.
Expressing the most general type of apply--that's not a super-type--is a
complicated process. It is clear that a large library of type functions will
likely be necessary, I think. This can be used as an argument both for and
against dependant types.
It is, however, also clear that when in using dependant types, much more
type information and documentation are provided. If, in fact, the example
from above can be type checked (question [2]), then it is clear that
dependant types are a *huge* bonus to more formally developing programs.
Since essentially anything (well, minus partial functions and some other
good things) can be specified in Lof's type theory, it becomes possible for
the programmer to use formal methods to any extent he desires, with theorem
proving being equivalent to the program type checking. Well, actually it's
not quite so simple since because Cayenne does allow general recursion, you
can't actually trust the fact that your program type checks as proof it
follows the specification. This is something that I would appreciate if
Lennart elaborated on. To what extent is this a problem in practice? To what
extent will a program that type checks completely fail to follow its
specification? Can someone give specific examples?
Finally, I think that much insight is gained from reading the following
paper:
Luca Cardelli. "Structural subtyping and the notion of power type"
http://research.microsoft.com/Users/luca/Papers/StructuralSubtyping.pdf
http://research.microsoft.com/Users/luca/Papers/StructuralSubtyping.ps
(skip to the examples)
The paper is primarily about subtyping, but the examples the author gives
use dependant types. I think that his examples demonstrate that subtyping
and dependant types can be used as tools for programming *in the large.*
These two tools in conjunction with existentials and type classes hold the
promise of making Haskell's ability to define ADTs far more powerful.
On that note,
http://research.microsoft.com/Users/luca/Papers/PrimObjInterp.pdf
http://research.microsoft.com/Users/luca/Papers/PrimObjInterp.ps
Demonstrates quite clearly how programming in the large can benefit from
subtyping: inheritance and other OO idioms would be encodable in Haskell.
--
Finally, here is actual Cayenne code (straight from Lennart!) demonstrating
apply:
Here is how it would look in Cayenne (my Haskell-like language with
dependent types). It type checks and runs.
apply :: (a :: #) -> (b :: #) -> (l :: List a) -> ApplyType a b l -> b
apply a b (Nil) f = f
apply a b (p:ps) f = apply a b ps (f p)
ApplyType :: (a :: #) -> (b :: #) -> (List a) -> #
ApplyType a b (Nil) = b
ApplyType a b (_ : ps) = a -> ApplyType a b ps
Some things to note:
* Type variables are bound and passed explicitly (in this example).
* The type of all types is called #.
* There is no type deduction, only type checking, for this example.
* I had to change the order of the arguments to apply, since
later arguments can only depend on earlier ones.
* ApplyType is a function on that computes the type of the function
depending on the list. It is only use at compile time, never at run time.
