Categorial Types and OpenMath: Problems Found – Currying

• Currying inconsistencies in OpenMath

  • OMBind objects defined to be curried: ombind(q,x,y,e) := ombind(q,x,ombind(q,y,e))
  • OMApplication objects not curried: oma(ombind(lambda,x,y,f),a,b) :=? oma(ombind(lambda,x,ombind(lambda,y,f)),a,b)
  • Signatures are not curried: f:A,B->C vs. fmp[oma(eq,f,ombind(lambda,x,y,g))] => is (f(a) : B --> C) correct or not???
  • Multiple scopes for binder in curried OMBinding: ombind(q,x,ombind(q,y,e)) – q in and out of scope for x

• Currying as a universal categorial type inference rule would have avoided these problems (I conjecture)

Notes: