Nick Kallen <[EMAIL PROTECTED]> wrote:
> > 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
No, that's not what you want. :-) You want
apply :: (a -> a -> ... -> b) [a] -> b
I think the distinction is important (see below).
> F a * = member (map (F a) [0..]) // member [a] a -> Bool
I mave no clue what this means. What is `member'?
> and applyType can be defined more succinctly:
>
> applyType a l = F a (length l)
You can certainly express applyType that way in Cayenne if you
wish.
> 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
And that works in Cayenne as well (modulo the argument order).
> 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,
I agree, that's why you should have a b as the return type of apply.
The this comes for free and all the complications of apply
you go through are unnecessary.
> arity :: (F a *) -> Int
> arity (a -> as) = 1 + (arity as)
> arity a = 0
You cannot do this in Cayenne, there are no operations that scrutinize
types. They can only be built, and never examined or taken apart.
This is a deliberate design choice. The consequence is that type
cannot affect the control of a program, so they cannot really influence
the result of a program, and are thus needless at runtime.
> 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)))
Well, I'm lost again. :-)
> [1] What type can Cayenne infer for apply just given apply's definition?
Cayenne doesn't do type inference. Well, it does a little, but it
will punt on any recursive definitions. So you have to give the
type yourself. I guess it would be possible to do a little type
inference, but for a function like apply it would be difficult
(and impossible in general).
> [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?
Well, I don't really understand the definition, so I can't say.
But probably not since you've used the arity function.
> 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.
I don't think so. The type you want is (using your argument order)
apply :: (F a b (length l)) -> (l :: [a]) -> b
with
F a b 0 = b
F a b n = a -> F a b (n-1)
> 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?
It's trivial to construct examples. Take sorting
sort :: (l :: [a]) -> ComplicatedTypeToSpecifySorting l
Well, here's an implementation:
sort xs = sort xs
It's type correct, but doesn't really do what you want.
-- Lennart
