Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Leftover constraint when function return type is unknown #208

Open
MxmUrw opened this issue Feb 23, 2022 · 1 comment
Open

Leftover constraint when function return type is unknown #208

MxmUrw opened this issue Feb 23, 2022 · 1 comment
Labels
Frozen question Further information is requested unsolved constraint
Milestone

Comments

@MxmUrw
Copy link
Member

MxmUrw commented Feb 23, 2022

Take the following example:

function count(f:: Function, d::Matrix) :: Priv()
  (dim, _) = size(d)
  counter = 0
  for i in 1:dim
    dd = d[i,:]
    if f(dd) == 1
      counter = counter + 1
    else
      counter = clone(counter)
    end
  end
  counter
end

We get as result:

---------------------------------------------------------------------------
Type:
Fun([([Fun([([NoFun(Vector<n: τ_31, c: τ_10>[s_8](τ_82)) @ s_23] -> NoFun(τa_26)) @ Nothing]) @ (∞,∞),NoFun(Matrix<n: τ_31, c: τ_10>[s_9 × s_8](τ_82)) @ (∞,∞)] ->* NoFun(Num(Int[--]))) @ Just [Function,Matrix{Any}]])
---------------------------------------------------------------------------

in other words:

---------------------------------------------------------------------------
Type:
{
  -  {
    -  Vector<n: τ_31, c: τ_10>[s_8](τ_82)
        @ s_23
    --------------------------
     -> τa_26
  
  }
      @ (∞, ∞)
  
  -  Matrix<n: τ_31, c: τ_10>[s_9 × s_8](τ_82)
      @ (∞, ∞)
  --------------------------
   ->* Int[--]

}
---------------------------------------------------------------------------
Constraints:
   - top:
constr_7 : [final,worst,global,exact,special] IsTypeOpResult (Binary == (τa_26 @ η_17,Num(Int[1]) @ η_18) Bool)
   - others:

The actual question now is the constr_7 which we currently simply cannot resolve because τa_26 is the return type of the input function, and we thus have no idea what type it is.

What we might want to do is allow some kind of annotations for this case? Or resolve the == ops differently in the worst-case-solving?

@MxmUrw MxmUrw added the question Further information is requested label Mar 20, 2022
@MxmUrw
Copy link
Member Author

MxmUrw commented Apr 12, 2022

Since this constraint makes sense, we keep it like that for now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Frozen question Further information is requested unsolved constraint
Projects
None yet
Development

No branches or pull requests

2 participants