vjovanov / papers

Papers of Vojin Jovanovic.
http://vjovanov.com
0 stars 0 forks source link

Typechecking `@i?` #2

Open vjovanov opened 9 years ago

vjovanov commented 9 years ago

According to the current design of the type system we just use @i! and say that @i? means convert to inline if static. This is tricky though as bodies of methods that have @i? are hard to typecheck:

def f(x:Int @i?): Int @i? = 1 + x

This is solved by having a mechanism that evaluates all static values to inline. How about when we have:

def addOne(x: Int@i?):Int@i? = x + 1
def f(x:Int @i?): Int @i? = addOne(x)

How do we know here that types are OK? What if addOne was a third party library and did not have @i?. Would we have to promote it to inline conditionally, or we should reject that program?

vjovanov commented 9 years ago

/cc @densh

densh commented 9 years ago

I'd say desugar @i? annotated types into generics:

def f(x: Foo @i?) = t
--->
[F <: Foo] => (x: F) => t

Then a type system should be able to do all the work for you (provided there is type inference, of course.)

vjovanov commented 9 years ago

Let's discuss when you are here.

densh commented 9 years ago

We decided to drop @i?, didn't we? Can we close the issue now?