search

evincarofautumn / kitten

A statically typed concatenative systems programming language.
http://kittenlang.org/
Other
1.09k stars 39 forks source link

Allow restricted higher-rank polymorphism #58

Closed evincarofautumn closed 10 years ago

evincarofautumn commented 11 years ago

It should be possible to write this function:

def trip (a a (a a -> a) -> (a & a & a)):
  -> { a b f }
  a b f@
  a b f@
  a b f@
  pair pair

But its type is:

∀r s a. r a a (s a a → s a) → r (a & a & a))

When it should be the rank-2:

∀r a. r a a (∀s. a a → s a) → r (a & a & a))

So the compiler complains because f is applied to different stack types.

strager commented 11 years ago

Why not this?

def trip (a a (a a -> a) -> (a & a & a)):
  -> { a b f }
  a b f@  // fat
  dup dup
  pair pair

Or is it just a bad example?

kchaloux commented 11 years ago

There is already a workaround for it:

def trip (a a (a a -> a) -> (a & a & a)):
  -> { a b c }
  a b f@ -> x
  a b f@ -> y
  a b f@ -> z
  x y z pair pair

But the behavior that most would probably expect would be for invocations of f to still be valid when applied multiple times, the same way any normal local can be pushed onto the stack multiple times after it is bound.