The inductive representation of Nat is problematic because a + b will be computed through recursion. Currently, computing 2 + 2 in the inductive representation takes around 23k iterations. Computing 2 + 2 natively takes 3 iterations. For small values, the inductive representation is still acceptable. However, the definition of Char encodes Nat values >50k. And we have native chars in Lurk! Hence it makes the most sense to replace Nat/Char/String with Lurk primitives.
How
[ ] Detect Nat/Char/String in Yatima IR at transpile time and transpile them as primitives. For example, def two := 2 will look like def two := OfNat.ofNat 2 in the IR. We need to strip the OfNat and directly use the Nat literal 2. The same applies for Chars and Strings
[ ] Seal off a core set of API with predefined Lurk functions. For example, we will define native addition lurk_Nat_add. Then, in transpilation, Nat_add should be ignored and every occurence of the Nat_add identifier should be replaced with lurk_Nat_add. We only need to do this for a few core functions, such that all other functions can be composed from the core set.
Why
The inductive representation of
Natis problematic becausea + bwill be computed through recursion. Currently, computing2 + 2in the inductive representation takes around 23k iterations. Computing2 + 2natively takes 3 iterations. For small values, the inductive representation is still acceptable. However, the definition ofCharencodesNatvalues >50k. And we have native chars in Lurk! Hence it makes the most sense to replaceNat/Char/Stringwith Lurk primitives.How
Nat/Char/Stringin Yatima IR at transpile time and transpile them as primitives. For example,def two := 2will look likedef two := OfNat.ofNat 2in the IR. We need to strip theOfNatand directly use theNatliteral2. The same applies forChars andStringslurk_Nat_add. Then, in transpilation,Nat_addshould be ignored and every occurence of theNat_addidentifier should be replaced withlurk_Nat_add. We only need to do this for a few core functions, such that all other functions can be composed from the core set.