2. I tried playing around with the foo function I was working with
last time, and am getting a different error now:
foo :: Int - [Char]
foo 0 = []
foo x = ['1'] ++ foo(x div 10)
You should have typed "9 div 3" at the listener and you'd have figured out
your error. No infix
Watch out here; there may be a limit to how much run-time type
inspection it is reasonable to do in the presence of dependent types.
Suppose you're examining a type which happens to be the type of some
sorting function:
(Ord a) = (l :: [a]) - ((l' :: [a]), sorted l l')
How much type
On 24-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote:
Fergus Henderson [EMAIL PROTECTED] writes:
What if the body of min2 were defined so that it returned
something different in the two cases? Your code has no proof that the
code for the two cases is equivalent. If it's not, then
If this is true, then what I'm doing is horrible. But I don't
see how this
leads to nondeterminism or broken referential transparency.
min2 returns the
same value for the same list, but it's simply more efficient
if we happen to
know some more information about the list.
In
I don't understand. What behaviour is different here?
Certainly the type is different. But how is the behaviour different?
It behaves differently in that it accepts and returns more/less values. If
this function is part of a program, then the behavior of the program is now
different in that
If you return the same proof of correctness that you used
for the earlier definition of sort, then no it won't type check.
But if you return a proof defined as e.g.
proof = proof
then if I understand things correctly it will type check.
On that note, since this has been of
apply :: (F a *) [a] - (F a *)
apply f [] = a
apply f [a:as] = apply (f a) as
The type gets noisier.
(To correct a couple of minor typos, that should be
apply f [] = f
apply f (a:as) = apply (f a) as
)
Heh, thank you. :)
I agree it is in some sense six of one and
What is the general consensus on views and the extended pattern guards that
are discussed at
http://www.haskell.org/development/ ?
I think views are really neat, but am not quite sure how I feel about
pattern guards.
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
If your language supports optional dynamic type checking, as it should,
then expressing functions like apply shouldn't be too hard.
Here's a dynamic apply in a pseudo Clean 2.0 syntax:
apply :: Dynamic [a] - a
apply (f :: a - b) (arg:args) = apply (dynamic (f arg) :: b) args
apply (f :: a) []
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
11 matches
Mail list logo
