HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.55k stars 141 forks source link

Inconsistent arity error #582

Closed sw1sh closed 2 months ago

sw1sh commented 9 months ago

Trying to implement SK combinators (is there a way to simplify it and make more readable?):

#derive[match]
type C {
  S
  K
  Ap (x : C) (y : C)
}

Reduce (a : C) : C
Reduce C.S = C.S
Reduce C.K = C.K
Reduce (C.Ap a b) = Reduce (match C a {
  S => C.Ap C.S (Reduce b)
  K => C.Ap C.K (Reduce b)
  Ap (x=c) (y=d) => match C c {
    S => C.Ap C.S (Reduce d)
    K => d
    Ap (x=e) (y=f) => match C e {
      S => C.Ap (C.Ap f b) (C.Ap d b)
      K => C.Ap C.K (Reduce f)
      Ap (x=g) (y=h) => C.Ap (Reduce g) (Reduce h)
    }
  }
})

// s[s[s]][s][s][s][s[s][k[k]]]
Main {
  // Reduce (C.Ap (C.Ap (C.Ap (C.Ap (C.Ap (C.Ap C.S (C.Ap C.S C.S)) C.S) C.S) C.S) (C.Ap C.S C.S)) (C.Ap C.K C.K))
  Reduce (C.Ap (C.Ap C.K C.K) C.K)
}
> kind2 run sk.kind2

CHECKING  The file 'sk.kind2'

[Error]: internal compiler error 'inconsistent arity on: '(Ap x0.0 x1.0)'' at /Users/swish/.cargo/registry/src/index.crates.io-6f17d22bba15001f/hvm-1.0.10/src/language/rulebook.rs:95:15
Please submit a full report about this error at: https://github.com/HigherOrderCO/Kind/issues/new
It would help us a lot :)
kings177 commented 2 months ago

Sorry for the late response, this iteration of kind2 has been superseded by kind2, closing this since we are restoring this repo to the old kind-legacy.