dfinity / motoko

Simple high-level language for writing Internet Computer canisters
Apache License 2.0
512 stars 97 forks source link

Stack overflow in type checking #3135

Closed wewei closed 2 years ago

wewei commented 2 years ago

Motoko Version

Motoko 0.6.21 (source wahvzdqw-grg3wqkh-0n8s7fj6-f4rxx0rh)

Repro Steps

  1. Copy & paste the problematic code snippet into chain.mo
  2. Try to run the code with moc -r --package base $(dfx cache show)/base chain.mo

Expects

No crash, print out #ok(123)

Actual

moc crashes, refer to crash_log.txt for detail

Problematic Code

import Result "mo:base/Result";
import Debug "mo:base/Debug";

type R<V, E> = Result.Result<V, E>;

type ResultChain<A, E> = {
  then: <B>(A -> R<B, E>) -> ResultChain<B, E>;
  value: R<A, E>;
};

func chain<A, E>(value: R<A, E>) {
  {
    then = func <B>(f: A -> R<B, E>): ResultChain<B, E> {
      switch value {
        case (#err(e)) { #err(e) };
        case (#ok(a)) { chain(f(a)) };
      }
    };
    value;
  }
};

Debug.print(debug_show(chain(#ok(123)).value));
ggreif commented 2 years ago

Thanks for the report, this looks like a duplicate of #3057.

ggreif commented 2 years ago

I am amazed how the functor/monad mindset already penetrated the IC space!

ggreif commented 2 years ago

Closing as a duplicate.

ggreif commented 2 years ago

Let me add some context. We have some code in moc (the expansiveness check) that rules out types (better: type constructors like your ResultChain) that have type parameters different from those in the head of the definition (here ResultChain<A, E>, and later used as ResultChain<B, E>). This is meant to catch polymorphic recursion, as it would lead to structurally infinite types, and (as we suspect) is also at odds with subtyping. In this case the expansiveness check seems to malfunction, descending into an infinite recursion.

But I am a bit puzzled about what you are tying to accomplish here. It seems to me that you want a generic interface for chainable things, but OTOH you hard-code R, a.k.a. Result.Result, into it. That doesn't buy you anything (other than a wrapping layer), as you cannot abstract away from R (technically Motoko doesn't support higher-kinded-polymorphism like Haskell).

So I can only suggest to use the top-level chain function provided by mo:base/Result.

wewei commented 2 years ago

I am amazed how the functor/monad mindset already penetrated the IC space!

Yeah, it took me too many lines to deal with error checking. I really love the Haskell way. Everybody love the Haskell way.

wewei commented 2 years ago

Let me add some context. We have some code in moc (the expansiveness check) that rules out types (better: type constructors like your ResultChain) that have type parameters different from those in the head of the definition (here ResultChain<A, E>, and later used as ResultChain<B, E>). This is meant to catch polymorphic recursion, as it would lead to structurally infinite types, and (as we suspect) is also at odds with subtyping. In this case the expansiveness check seems to malfunction, descending into an infinite recursion.

But I am a bit puzzled about what you are tying to accomplish here. It seems to me that you want a generic interface for chainable things, but OTOH you hard-code R, a.k.a. Result.Result, into it. That doesn't buy you anything (other than a wrapping layer), as you cannot abstract away from R (technically Motoko doesn't support higher-kinded-polymorphism like Haskell).

So I can only suggest to use the top-level chain function provided by mo:base/Result.

The type R is just a type alias to make the code shorter. What I want to do have is something like this

switch (
  chain<A, Text>(getA) // where getA may return an #err("Some error getting A")
    .then<B>(getBFromA) // where getBFromA may return an #err("Something wrong getting B")
    .then<C>(getCFromB) // there may be errors as well
    .value
) {
  case (#ok(c)) { /* do something with c */ };
  case (#err(msg)) { /* report the error */ };
}

HKT is a nice feature, however, I fully understand it's not the priority for now.

I can use the chain function in mo:base/Result, but that would create an onion of parentheses. Another problem of the chain in Result is it has 3 generic parameters. I found the type inference is not as convenient as mature languages like TypeScript. I usually need to pass the generic parameters explicitly. Having too many parameters would make the code longer, which impacts the readability.

wewei commented 2 years ago

BTW, here's the code snippet I had trouble with (too many indentations)

public shared({ caller }) func buy(list: [(Nat, Nat, Nat)], tokens: Nat): async R<Inventory> {
    switch (userMap.getValue<Inventory>(inventories, caller)) {
      case (null) {#err(ERR_USER_NOT_FOUND) };
      case (?inventory) {
        if (inventory.tokens < tokens) {
          #err(ERR_INSUFFICIENT_TOKENS)
        } else {
          Result.chain<Nat, Inventory, Text>(
            priceForList(list),
            func (realtimePrice) {
              if (realtimePrice > tokens) {
                #err(ERR_PRICE_CHANGED)
              } else {
                let (tokens, _) = LN.safeSub(inventory.tokens, realtimePrice);
                Result.chain<Map<Nat, (Nat, Nat)>, Inventory, Text>(
                  foldLeft<(Nat, Nat, Nat), R<Map<Nat, (Nat, Nat)>>>(
                    list,
                    #ok(inventory.crops),
                    incCrops),
                  func (crops) {
                    let newInventory = { tokens; crops };
                    inventories := userMap.putKeyValue<Inventory>(inventories, caller, newInventory);
                    #ok(newInventory)
                  }
                )
              }
            }
          )
        }
      };
    }
  };
crusso commented 2 years ago

You might be able to avoid some of those type parameters if you, instead, annotate the argument and result types of the lambdas func (realtime) ... and func (crops) ... but I haven't done the experiment.

Motoko type inference is certainly not as powerful as ML or Haskell, unfortunately.

We've contemplated adding a form of general, monadic do syntax to Motoko in the past, and may get around to it at some point, but it's not high priority just now.