DiffMu / DiffPrivacyInferenceHs

BSD 3-Clause "New" or "Revised" License
0 stars 0 forks source link

subtyping assumes numeric type hierarchy has top and bottom #247

Open ooovi opened 2 years ago

ooovi commented 2 years ago

but since we have data, that's not the case anymore.

ooovi commented 2 years ago
 typecheck_hs_from_string("
       module L
       function testScale(_, x, xs)
                        _ = clone(x)              
                       (dim, _) = size(xs)        
                       dim + x                    
                    end 
                    end")
======================== Errors =====================

======================== End Errors =====================

---------------------------------------------------------------------------
Type:
{
  -  τ_12
      @ ∑∅

  -  τ_15[--]
      @ 1

  -  Matrix<n: τ_8, c: τ_9>[s_3 × s_4](τ_7)
      @ ∑∅
  --------------------------
   -> τ_16[--]

}
---------------------------------------------------------------------------
Constraints:
   - top:
constr_5 : IsSupremum (Int,τ_15) :=: τ_16
  Inherited from the constraint:
     IsTypeOpResult (Binary + (Num(Int[s_3 ©]) @ η_1,Num(τ_15[--]) @ η_2) Num(τ_16[--]))
  In none: line 6
  Constraint on the builtin call:
  dim + x

   - others:
[]
()

removing this left us with unresolved constraints that could be resolved. oh well.

ooovi commented 2 years ago

a solution would be another layer in our number types, having a separate kind for [Real Int] and Data. Both kinds have top and bottom, and we could use the trick again :)

ooovi commented 2 years ago

i added a few type annotations that would become unneccesary if we did this and also disabled a few tests in commit a8f0bff if we ever do this we should reenable/deannotate