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

Add dependent function types #3464

Merged
merged 13 commits into from Nov 27, 2017

Conversation

Projects
None yet
6 participants
@odersky
Contributor

odersky commented Nov 12, 2017

We now support dependent function types as long as there are no inter-parameter dependencies.
Assuming

class C { type T }

a dependent function type is written like this:

 (x: C) => x.T

It gets represented as a normal function type that approximates the result type together with a refinement that adds an apply method with the precise type. E.g. the type above would be represented as

Function1[C, C#T] { def apply(x: C): x.T }

For the moment, dependent function types cannot be implicit. Maybe we can lift that restriction in the future.

Dependent function types are important, because they are already in DOT, and they are probably a key feature to enable polymorphic effect systems.

@nicolasstucki

This comment has been minimized.

Show comment
Hide comment
@nicolasstucki

nicolasstucki Nov 13, 2017

Contributor

We should have some neg tests for implicit dependent function types.

Contributor

nicolasstucki commented Nov 13, 2017

We should have some neg tests for implicit dependent function types.

@odersky odersky requested a review from OlivierBlanvillain Nov 13, 2017

@LPTK

This comment has been minimized.

Show comment
Hide comment
@LPTK

LPTK Nov 14, 2017

This is great. Now we can almost have a nice first-class polymorphic lambda syntax.

> def baz(f: (t: C) => List[t.T] => List[t.T]): Int = 
    f(new C{type T = Int})(List(1,2,3)).head
> baz(t => (ls:List[t.T]) => ls.reverse)
res0: Int = 3

Unfortunately, we currently need to explicitly state the type of ls, and also the whole thing stops working when t is made implicit.

Ideally, is it reasonable to expect the following program to work?

def baz(f: implicit (t: C) => List[t.T] => List[t.T]): Int = f(new C{type T = Int})(List(1,2,3)).head
baz(ls => ls.reverse)

LPTK commented Nov 14, 2017

This is great. Now we can almost have a nice first-class polymorphic lambda syntax.

> def baz(f: (t: C) => List[t.T] => List[t.T]): Int = 
    f(new C{type T = Int})(List(1,2,3)).head
> baz(t => (ls:List[t.T]) => ls.reverse)
res0: Int = 3

Unfortunately, we currently need to explicitly state the type of ls, and also the whole thing stops working when t is made implicit.

Ideally, is it reasonable to expect the following program to work?

def baz(f: implicit (t: C) => List[t.T] => List[t.T]): Int = f(new C{type T = Int})(List(1,2,3)).head
baz(ls => ls.reverse)
Show outdated Hide outdated compiler/src/dotty/tools/dotc/typer/Inferencing.scala
ParamRefNameString(tp) ~ ".type"
case tp: TypeParamRef =>
ParamRefNameString(tp) ~ lambdaHash(tp.binder)
case tp: SingletonType =>

This comment has been minimized.

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

I think something is wrong with the way dependent function types are printed:

scala> val depfun1: DF = (x: C) => x.m
val depfun1: (C => ){apply: (x: C): } = <function1>
@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

I think something is wrong with the way dependent function types are printed:

scala> val depfun1: DF = (x: C) => x.m
val depfun1: (C => ){apply: (x: C): } = <function1>

This comment has been minimized.

@odersky

odersky Nov 15, 2017

Contributor

Should be fixed now.

@odersky

odersky Nov 15, 2017

Contributor

Should be fixed now.

// Reproduced here because the one from DottyPredef is lacking a Tasty tree and
// therefore can't be inlined when testing non-bootstrapped.
// But inlining `implicitly` is vital to make the definition of `ifun` below work.
inline final def implicitly[T](implicit ev: T): T = ev

This comment has been minimized.

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

Would changing implicitly to return ev.type instead of T help here?

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

Would changing implicitly to return ev.type instead of T help here?

This comment has been minimized.

@smarter

smarter Nov 14, 2017

Member

The fact that adding inline changes how a method is typechecked doesn't seem like a great thing. I think @OlivierBlanvillain has some examples where it breaks working code.

@smarter

smarter Nov 14, 2017

Member

The fact that adding inline changes how a method is typechecked doesn't seem like a great thing. I think @OlivierBlanvillain has some examples where it breaks working code.

This comment has been minimized.

@odersky

odersky Nov 15, 2017

Contributor

I am a bit nervous about changing it to ev.type. The inferencer has to do major acrobatics to deal with implicit method types. It might interfere with something else. The current type of implicitly is simpler and clearer.

@odersky

odersky Nov 15, 2017

Contributor

I am a bit nervous about changing it to ev.type. The inferencer has to do major acrobatics to deal with implicit method types. It might interfere with something else. The current type of implicitly is simpler and clearer.

Show outdated Hide outdated compiler/src/dotty/tools/dotc/typer/Typer.scala
args match {
case ValDef(_, _, _) :: _ =>
typedDependent(args.asInstanceOf[List[ValDef]])(

This comment has been minimized.

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

I'm a bit confused by this cast, args matches ValDef() and is casted to a List[ValDef]??

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

I'm a bit confused by this cast, args matches ValDef() and is casted to a List[ValDef]??

This comment has been minimized.

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

Oh I didn't see the ::

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

Oh I didn't see the ::

Show outdated Hide outdated compiler/src/dotty/tools/dotc/typer/Typer.scala
trait C { type M; val m: M }
type DF = (x: C) => x.M
val depfun1: DF = (x: C) => x.m

This comment has been minimized.

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

I like than both the type and the value have the same syntax :)

@OlivierBlanvillain

OlivierBlanvillain Nov 14, 2017

Contributor

I like than both the type and the value have the same syntax :)

This comment has been minimized.

@esarbe

esarbe Nov 21, 2017

Contributor

Yes. This is something that I really like about Scala in general.

@esarbe

esarbe Nov 21, 2017

Contributor

Yes. This is something that I really like about Scala in general.

odersky added some commits Nov 12, 2017

Drop AllowDependendFunctions mode bit
Tests indicate it's not needed anymore.

Also: fix neg test error position.
Dependent function types may not be implicit
For the moment we want to rule this out. There are quite a lot of
bits we have to think through before we can allow this.
Fix problem with partly uninstantiated dependent functions
If the result type of a dependent function contains a type variable whose bounds
refer to the function's parameters, that type variable has to be instantiated before
the method type is formed. Otherwise, if the type variable is instantiated later
the method result type will refer to the original parameter symbols instead of
the method types ParamRefs.
Refine isFunctionType
`isFunctionType` nor returns true for dependent as well as non-dependent
function types. `isNonDepFunctionType` returns true only for the latter.
Fix printing of TermParamRefs
The change that TermParamRefs are Singletons caused a change how they are printed,
which this commit reverts.

We had before

    def f(x: T): x.type
    def f(x: T): x.type # M

Once TermParamRefs were singletons we got:

    def f(x: T): T (x)
    def f(x: T): x.M

With this commit we now get:

    def f(x: T): x.type
    def f(x: T): x.M
Add case for Inlined to TypedTreeCopier
The missing case was discovered after inlining `implicitly`. It produced
a type mismatch in Ycheck after lambda lift.
Improve type inference for dependent function types
Given a dependently typed function value like this one:

    def f: (x: C) => D => x.T => E

we did not propagate information about the subsequent types `D` and `x.T` to
the result type of the closure with parameter `(x: C)`. Doing so is a bit
tricky because of the dependency. But it's necessary to infer the
types of subsequent parameters.

Test case: eff-dependent.scala

@odersky odersky merged commit 817fe72 into lampepfl:master Nov 27, 2017

2 checks passed

CLA User signed CLA
Details
continuous-integration/drone/pr the build was successful
Details

@liufengyun liufengyun deleted the dotty-staging:add-depfuns branch Nov 29, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment