Safer Anoma decoding proposal

[janmasrovira]

The current type of the primitive anomaDecode is equivalent to:

anomaDecode {T} (encoded : Nat) -> T;

If the encoded natural cannot be decoded into a term of type T it will crash, which can be problematic.

We have discussed some solutions to the problem and we have agreed (at least on the general idea) to proceed as follows:

1. The axiom will change to the following

   unsafeAnomaDecode {T} (encoded : Nat) -> Maybe T;
   

   This is marked as unsafe because we can only check that the decoded term has the shape of some term of T, however, this could be coincidental (E.g. Bool and Nat are overlapping on their nockma encodings).

   To make the problem more explicit we would expose the following definitions:

   type DecodeResult (A : Type) :=
      decodeFail
      | decodeSameShape A;
      
   anomaDecode {T} : (encoded : Nat) -> DecodeResult T := unsafeAnomaDecode >> maybe decodeFail decodeSameShape;
   

2. Then the users might add a unique type identifier to make decoding safer. E.g.

   MyArgumentsUid : Nat := 1238772879238821273;
   
   type MyArguments := mkArgs {
     uid : Nat   -- should always be set to MyArgumentsUid
     arg1 : ...
     ...
   };
   
   
   myDecode {A} (x : Nat) : Maybe A := case decode x of
     Fail := error "no match"
     SameShape args
         | if uid args == MyArgumentsUid := ok args
         | else := error "type uid does not match";
   

Extension 1 (derived type uid)

• In order to facilitate the above strategy, the juvix compiler could provide a primitive that would return some uid for any type. The details of how we should compute this uid are to be discussed.

  typeUid : Type -> Nat;
  

  Another option would be to define a trait and support deriving it.

  trait 
  type HasUid (A : Type) := mkHasUid@{
     getTypeUid : Nat
   };
  

Extension 2 (default arguments for record types)

• Default values for record fields #2427. With default arguments for record types we could make it so that the uid type is pupulated with the desired value by default.

  type MyArguments := mkArgs {
      {uid} : Nat := MyArgumentsUid;
      arg1 : ...
      ...
    };