We might want to have functions polymorphic over sensitivities

[MxmUrw]

The following example cannot be checked because the function f is not polymorphic over the constant value of the argument y.

julia> typecheck_hs_from_string("module mod
       function create_query(b,query)
              m -> query(m, b) - query(m, b+1)
             end
             function foo(bb)
                function f(x,y)
                  a = internal_expect_const(y)
                  3 + a
                end
                create_query(internal_expect_const(bb),f)
             end
             end
             ")
======================== Errors =====================
Error:
Could not unify 's_15' with '1 + s_15'.
  The constraint constr_49 : IsEqual (s_15,1 + s_15)
  could not be solved:
  ---------------------------------------------------------
  Inherited from the constraint:
     IsLessEqual (s_15 ©,1 + s_15 ©)
  Inherited from the constraint:
     IsLessEqual (τ_44[s_15 ©],τ_30[1 + s_15 ©])
  Inherited from the constraint:
     IsLessEqual (Num(τ_44[s_15 ©]),Num(τ_30[1 + s_15 ©]))
  Inherited from the constraint:
     IsSupremum (NoFun(Num(τ_44[s_15 ©])),NoFun(Num(τ_44[1 + s_15 ©]))) :=: NoFun(Num(τ_30[1 + s_15 ©]))
  Inherited from the constraint:
     IsChoice (fromList [([Any,Any],(([τ_21 @ ∑∅,NoFun(Num(τ_30[1 + s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))),[]))],[([τ_8 @ ∑∅,NoFun(Num(τ_44[1 + s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))),([τ_4 @ ∑∅,NoFun(Num(τ_44[s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©])))])
  Inherited from the constraint:
     IsFunctionArgument (Fun([([τ_21 @ ∑∅,NoFun(Num(τ_30[1 + s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Just [Any,Any]]),Fun([([τ_8 @ ∑∅,NoFun(Num(τ_44[1 + s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Nothing,([τ_4 @ ∑∅,NoFun(Num(τ_44[s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Nothing]))
  Inherited from the constraint:
     IsChoice (fromList [([Any,Any],(([NoFun(Num(τ_44[s_15 ©])) @ ∑∅,Fun([([τ_8 @ ∑∅,NoFun(Num(τ_44[1 + s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Nothing,([τ_4 @ ∑∅,NoFun(Num(τ_44[s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Nothing]) @ ∑∅] -> Fun([([(τ_8∧τ_4) @ ∑∅] -> NoFun(Num(τ_31[(4.0 + s_15 - 4.0 + s_15) ©]))) @ Just [Any]])),[]))],[([NoFun(Num(τ_44[s_15 ©])) @ ∑∅,Fun([([τ_21 @ ∑∅,NoFun(Num(τ_30[1 + s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Just [Any,Any]]) @ ∑∅] -> τ_22)])
  Inherited from the constraint:
     IsFunctionArgument (Fun([([NoFun(Num(τ_44[s_15 ©])) @ ∑∅,Fun([([τ_8 @ ∑∅,NoFun(Num(τ_44[1 + s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Nothing,([τ_4 @ ∑∅,NoFun(Num(τ_44[s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Nothing]) @ ∑∅] -> Fun([([(τ_8∧τ_4) @ ∑∅] -> NoFun(Num(τ_31[(4.0 + s_15 - 4.0 + s_15) ©]))) @ Just [Any]])) @ Just [Any,Any]]),Fun([([NoFun(Num(τ_44[s_15 ©])) @ ∑∅,Fun([([τ_21 @ ∑∅,NoFun(Num(τ_30[1 + s_15 ©])) @ ∑∅] -> NoFun(Num(τ_30[4.0 + s_15 ©]))) @ Just [Any,Any]]) @ ∑∅] -> τ_22) @ Nothing]))
  In none: line 10
  The function  create_query is applied to [InternalExpectConst gen_bb_uls_3, f]
  ---------------------------------------------------------

[ooovi]

me favourite example:

# compute a (epsilon,0)-DP version of the average of a vector
function auto_avg(xs::Vector{<:Real}, bs::NoData(Vector), epsilon::NoData(Real)) :: Priv()

   # the query we want to make   
   clipped_sum(m,b) = fold((x,y) -> x+y, map(x -> clip(x,b,0.), m))

   # find suitable clipping parameter using svt
   function create_query(b)
      m -> clipped_sum(m, b) - clipped_sum(m, b+1)
   end

   queries = map(create_query, bs)

   epsilon_svt = epsilon / 3
   at = above_threshold(queries, epsilon_svt, xs, 0)
   final_b = bs[at]

   # compute noisy sum
   epsilon_sum = epsilon / 3
   noisy_sum = laplacian_mechanism(final_b, epsilon_sum, clipped_sum(xs, final_b))

   # compute noisy number of entries
   epsilon_count = epsilon / 3
   noisy_count = laplacian_mechanism(1, epsilon_count, length(xs))
   
   noisy_sum/noisy_count
end

sets the input vector bs to contain consts...

  -  Vector<n: L1, c: τ_8>[s_4](Real[--])
      @ (s_70, ∑∅)
  
  -  Vector<n: τ_142, c: τ_59>[s_66](Real[s_9 ©])
      @ (∞, ∞)
  
  -  τ_281[s_70 ©]
      @ (∑∅, ∑∅)
  --------------------------
   ->* Real[--]