_at_Sebastian Fischer
> differently. So, maybe "cursor :: a" should be the correct type, even
> if mz was a free variable (?)
No. A monomorphism restriction on free variables is the right thing.
They are just non-canonical elements of a type which might be replaced
by computed values. Let's put it this way: Logic variables allow a
/single assignment/. And so do their associated type-variables.
_at_Wolfgang Lux
> The Curry type checker *is* correct (I'm sure, since I wrote it :-).
No, it's not. Sebastian Fischer digged it out. Every call to the
'unknown' function will give you a fresh, free variable (I think it's
like with IO References in Haskell). But since they can be bound -
shared or not - to values, the context of their occurrence may fix their
type.
But
bot :: a
bot = bot
will never compute to any value at all. And that's why /statically/ you
can use it everywhere.
Like I wrote earlier, it inhabits the /intersection of all types/. So it
really has the type:
bot :: forall a. a
The Curry type-checker doesn't infer a most general type for it, when
binding the type-variable due to context.
There's something like a 'polymorphism restriction' to it.
Please note that I was the last man wanting this discussion. On the
contrary, I was proposing something which I thought was a nice
workaround (maybe a bit more than that) for using bottom to make
partially implemented programs checkable, relying on a feature which is
very idiomatic Curry - monomorphic, free variables.
_at_Claus Reinke
> Here is Bernd's variant translated to Haskell, using lambda-binding instead
> of let-binding for the things whose types we want information on:
[...]
> no "free", just parameterized by the unknowns z and s. now we can load
Well, almost exactly the same program was already contained in my
initial post...
> this into GHCi, and get:
>
> *Main> :t cursor undefined undefined
> cursor undefined undefined :: (Nat -> Nat, (Nat -> Nat) -> Nat -> Nat)
But what is this good for, I asked? Think about what happened when you
handed in your maths excercises that way: basis and inductive step not
separated (and no proof of either one).
_at_Bernd Brassel
> Now you get for the type of cursor:
>
> cursor :: (Nat -> Nat,(Nat -> Nat) -> Nat -> Nat)
>
> and some thinking gives us
>
> plus = foldNat id (S .)
>
> Right?
Yes and No. It's just not the case that I had wanted to inform the Curry
community that I found that 'a compiler can infer types for you'.
All I wanted to do was demonstrating how free variables make it very
easy to focus the type-checker on sub-programs *one-at-a-time*. And also
that shifting that focus requires no more rewriting than changing a
variable.
It's about explaining where programs do come from:
Make up your mind what kind of things you want to feed to your program
and what you expect it to return. Write that down.
myprog :: T1 -> T2 -> ... -> T(n-1) -> Tn
myprog = undefined -- back by popular demand
Now take away an interesting argument, may be the first one ...
myprog :: T1 -> T2 -> ... -> T(n-1) -> Tn
myprog = \t1 -> undefined
...and proceed in the canonical way of writing programs with elements of
this type. For the naturals this happens to be primitive recursion.
Others may be part of the prelude.
This might require you to write several sub-programs which to abstract
first could be convenient.
myprog :: T1 -> T2 -> ... -> T(n-1) -> Tn
myprog = \t1 -> elimT1 t1 s2 ... s(k-1)
where s2,...,s(k-1) free
Now aim to solve sub-tasks *one-at-a-time*
cursor = s2
where
myprog :: T1 -> T2 -> ... -> T(n-1) -> Tn
myprog = \t1 -> elimT1 t1 s2 ... s(k-1)
s2,...,s(k-1) free
with the machine providing only information being /relevant/ at this
point.
cursor :: S2 [Sk/T2 -> ... T(n-1) -> Tn]
cursor = s2
where
myprog :: T1 -> T2 -> ... -> T(n-1) -> Tn
myprog = \t1 -> elimT1 t1 s2 ... s(k-1)
s2,...,s(k-1) free
(given elimT1 :: T1 -> S2 -> ... -> S(k-1) -> Sk)
Iterate this process for the inititial sub-problems and and the ones
emerging from the solution to the first.
I knew that a program changing its type as heavily as the 'cursor' might
look odd.
That's why I made the screencast: to show that there's really not so
much to it. You see nothing but my editor all the time with two
shell-outs to the addtypes tool with subsequent reloads of the file.
And since there's no creativity involved, I turned on a hand-writing
font to make it look a bit more loose.
> Old School says, first thing about writing a function is its type. To
Which might just be the flavour of the month. For example, when writing
polymorphic recursive programs you won't get around giving a signature.
So why not start with it anyway?
Thanks for the addtypes tool, Bernd! I'm having fun with it. It's just
that I don't want to apply it to my completed programs afterwards, but
to integrate it into the process of programming.
Cheers,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mo Dez 18 2006 - 11:00:50 CET