ponylang / ponyc

Pony is an open-source, actor-model, capabilities-secure, high performance programming language
http://www.ponylang.io
BSD 2-Clause "Simplified" License
5.71k stars 415 forks source link

Can't feasibly use iftype to specialize the body of a method that returns the type param. #2121

Open jemc opened 7 years ago

jemc commented 7 years ago

This is a pain point I ran into with the experimental iftype feature, where I'd expect the following to compile, but it doesn't:

type JSONAny is (F64 | I64 | Bool | None | String | JSONArray | JSONObject)

primitive JSON
  fun parse[J: JSONAny val = JSONAny](
    string: String,
    offset: USize = 0,
    length: USize = -1)
    : J ?
  =>
    iftype J <: F64 val then F64(0)
    elseif J <: I64 val then I64(0)
    elseif J <: Bool val then true
    elseif J <: None val then None
    elseif J <: String val then ""
    elseif J <: JSONArray val then recover JSONArray end
    elseif J <: JSONObject val then recover JSONObject end
    else error
    end

class val JSONArray
class val JSONObject
jemc commented 7 years ago

@Praetonus have any thoughts on this one?

Praetonus commented 7 years ago

It looks like a bug, I think it should work.

plietar commented 7 years ago

I don't think this snippet can be made to work as is.

The iftype expression has type (F64|I64|Bool|None|String|JSONArray|JSONObject), which needs to be a subtype of J. Instead you need to coerce the values to J before leaving the iftype branch: https://is.gd/Lt3LFv

primitive JSON
  fun _coerce[J](x: J) : J => consume x

  fun parse[J: JSONAny val](): J ? =>
    iftype J <: F64 val then _coerce[J](F64(0))
    elseif J <: I64 val then _coerce[J](I64(0))
    elseif J <: Bool val then _coerce[J](true)
    elseif J <: None val then _coerce[J](None)
    elseif J <: String val then _coerce[J]("")
    elseif J <: JSONArray val then _coerce[J](recover JSONArray end)
    elseif J <: JSONObject val then _coerce[J](recover JSONObject end)
    else error
    end

After that you are left with proving that (J val | J val | J val | J val | J val | J val | J val) <: J val, except each J (call these J0, J1, ...) of that union type is actually a distinct type variable (because of how iftype is implemented) , different from the outer J.

You would therefore need J0 <: J, J1 <: J, ... Each type variable's ast_data points back to the "root" typevariable, so changing is_typeparam_sub_typeparam to the following makes it work, as it will consider the two type variables identical :

  ast_t* sub_def = (ast_t*)ast_data(sub);
  sub_def = ast_data(sub_def);

  ast_t* super_def = (ast_t*)ast_data(super);
  super_def = ast_data(super_def);
jemc commented 7 years ago

There was some brief brainstorming at the end of today's sync calls about how this might be made to work without needing the _coerce workaround.

So far nothing concrete to go on, other than one idea I had about typechecking the entire body of the method against each iftype assumption. @sylvanc agreed that this would work, but would be a "combinatorial explosion" in runtime typechecking work.