> > 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'?
Member is memq, in, etc. Checks for membership in a list.
"F a *" is a predicate on types. It's a magical syntax, not valid Haskell.
It checks to see if the type is in the list:
[a, a -> a, a -> a -> a, a -> a -> a -> a, ...]
> > 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.
I'd like to make an argument against that. Like Fergus I am an advocate of a
dynamic types. (I've never met a type system I didn't like ;). To add
dynamic types to a language, you can make them a special feature, with some
sort of "dynamic" type constructor, and pattern match like:
draw :: Dynamic -> Picture
draw (c :: Circle) = drawCircle c
draw (s :: Square) = drawSquare c
...
draw (u :: _) = theEmptyPicture // What happens if you try to draw a "file"?
(I'm not sure on the syntax of how existing Haskell implementations support
this. The above is largely based on the Clean 2.0 syntax.)
The whole idea behind dynamic types is that run-time type information can be
inspected and manipulated.
You can add dependant types to Cayenne (theoretically) just by allowing the
run-time type inspection that you intentionally disallowed. In my mind,
you'd kill two birds with one stone.
> > 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. :-)
Well, especially since there's an error, it might lead to confusion.
let me redefine Fr:
Fr a l = member (map (F a) l)
so
Fr a [1, 4, 6] == member [a -> a, a -> a -> a -> a -> a, a -> a -> a -> a ->
a -> a -> a].
Given the same type of apply, I'll restate it in words:
f is of arity >= length l. The range of apply is of arity ((arity f) -
(length l)).
> > [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).
The obvious question: does "in general" equal "in practice"?
> > [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.
Right. it relies on run-time type information.
> > 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.
but if you say
sort [] = []
sort (x:xs) = sort elts_lt_x ++ [x] ++ sort elts_greq_x
where
elts_lt_x = [y | y <- xs, y < x]
elts_greq_x = [y | y <- xs, y >= x]
will the type checker say "yes," and can you believe it?
What if you do this:
sort (x:xs) = sort elts_lt_x ++ sort elts_greq_x
where
elts_lt_x = [y | y <- xs, y < x]
elts_greq_x = [y | y <- xs, y >= x]
(i.e., you leave out the pivot [x])
Obviously the result of sort will no longer be a permutation of its
argument. Will this then not type check?
