Mentions légales du service

Skip to content
  • Andrei Paskevich's avatar
    Mlw: support Epure in the surface language (with type inference) · 72714897
    Andrei Paskevich authored
    The current syntax is "{| <term> |}", which is shorter than
    "pure { <term> }", and does not require a keyword. Better
    alternatives are welcome.
    
    As for type inference, we infer the type pf the term under Epure
    without binding destructible type variables in the program.
    In particular,
      let ghost fn x = {| x + 1 |}
    will not typecheck. Indeed, even if we detect that the result
    is [int], the type of the formal parameter [x[ is not inferred
    in the process, and thus stays at ['xi].
    
    Another problem is related to the fact that variable and function
    namespaces are not yet separated when we perform type inference.
    Thus both fuctions
      let ghost fn (x: int) = let x a = a in {| x + 5 |}
    and
      let ghost fn (x: int) = let x a = a in {| x 5 |}
    will not typecheck, since the type of [x] is ['a -> 'a] when
    we infer the type for the Epure term, but it becomes [int],
    when we construct the final program expression. Probably,
    the only reasonable solution is to keep variables and
    functions in the same namespace, so that [x] simply can
    not be used in annotations after being redefined as a
    program function.
    72714897