rodrigogribeiro / solcore

1 stars 2 forks source link

Function composition seems mistyped #3

Closed mbenke closed 2 months ago

mbenke commented 3 months ago

Consider a function composing its arguments:

contract Compose {
  function compose(f,g) {
    return lam (x) {
      return f(g(x));
    } ;   
  }

  function id(x) { return x; }

  function idid() { return compose(id,id); }

  function main() { return idid(42); }
/*
  function main() {
    let f = compose(id,id);
    return f(42);
  }
*/
}

It seems not to be typed right, consequently main gets wrong type:

Typing the call:f
Typing the call:g
Arguments: x :: j 
Result for call:g is l
Arguments: g(x) :: l 
Result for call:f is k
Before quantify:compose - h -> i -> j -> k
Results: compose :: forall a . h -> i -> j -> a

Typing the call:compose
Arguments: id :: r -> s id :: t -> u 
Result for call:compose is j -> p
Before quantify:idid - j -> p
Results: idid :: forall a . j -> a

Typing the call:idid
Arguments: 42 :: Word 
Result for call:idid is x
Before quantify:main - x
Results: main :: forall a . a

Before quantify:id - z -> z
Results: id :: z -> z

Also, why compose and main get quantified types, but id does not?

As a sidenote, I would like to write main as commented out, but cannot.

mbenke commented 3 months ago

See https://github.com/rodrigogribeiro/solcore/blob/specialisation/test/examples/spec/06comp.solc

rodrigogribeiro commented 2 months ago

Fixed on main.