- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Sebastian Hanowski <seha_at_informatik.uni-kiel.de>

Date: Mon, 18 Dec 2006 09:17:54 +0100

_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

Date: Mon, 18 Dec 2006 09:17:54 +0100

_at_Sebastian Fischer

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

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

[...]

Well, almost exactly the same program was already contained in my

initial post...

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

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.

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

*
This archive was generated by hypermail 2.3.0
: Sa Okt 16 2021 - 07:15:04 CEST
*