{"action":"created","issue":{"url":"https://api.github.com/repos/lampepfl/dotty/issues/3920","repository_url":"https://api.github.com/repos/lampepfl/dotty","labels_url":"https://api.github.com/repos/lampepfl/dotty/issues/3920/labels{/name}","comments_url":"https://api.github.com/repos/lampepfl/dotty/issues/3920/comments","events_url":"https://api.github.com/repos/lampepfl/dotty/issues/3920/events","html_url":"https://github.com/lampepfl/dotty/issues/3920","id":291854702,"number":3920,"title":"Dependent Class Types for Scala","user":{"login":"liufengyun","id":754633,"avatar_url":"https://avatars3.githubusercontent.com/u/754633?v=4","gravatar_id":"","url":"https://api.github.com/users/liufengyun","html_url":"https://github.com/liufengyun","followers_url":"https://api.github.com/users/liufengyun/followers","following_url":"https://api.github.com/users/liufengyun/following{/other_user}","gists_url":"https://api.github.com/users/liufengyun/gists{/gist_id}","starred_url":"https://api.github.com/users/liufengyun/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/liufengyun/subscriptions","organizations_url":"https://api.github.com/users/liufengyun/orgs","repos_url":"https://api.github.com/users/liufengyun/repos","events_url":"https://api.github.com/users/liufengyun/events{/privacy}","received_events_url":"https://api.github.com/users/liufengyun/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":19,"created_at":"2018-01-26T10:14:36Z","updated_at":"2018-02-04T12:26:09Z","closed_at":"2018-01-30T13:21:31Z","author_association":"CONTRIBUTOR","body":"# Dependent Class Types for Scala\r\n\r\n## Motivation\r\n\r\nScala already supports many variants of _dependent types_ (aka. types that depend on terms), e.g.\r\n\r\n- path-dependent types\r\n- dependent method types\r\n- dependent function types\r\n- singleton types\r\n- literal types\r\n\r\nThe combination of _higher-kinded types_ and _singleton types_ is another\r\ncommonly used approach to encode dependent types in Scala:\r\n\r\n```Scala\r\ntrait Context {\r\n  type Tree\r\n}\r\n\r\nclass Helper[T <: Context](val ctx: T) {\r\n  def f(x: Int): ctx.Tree = ???\r\n}\r\n\r\nval ctx  : Context   =  ???\r\nval tree : ctx.Tree  =  new Helper[ctx.type](ctx).f(5)\r\n```\r\n\r\nHowever, the encoding above is tedious in syntax. Instead, most programmers would\r\nexpect the following code to work:\r\n\r\n```Scala\r\ntrait Context {\r\n  type Tree\r\n}\r\n\r\nclass Helper(val ctx: Context) {\r\n  def f(x: Int): ctx.Tree = ???\r\n}\r\n\r\nval ctx  : Context   =  ???\r\nval tree : ctx.Tree  =  new Helper(ctx).f(5)\r\n```\r\n\r\nCompile the code above in Scala 2.12.4 will result in the following error message:\r\n\r\n```\r\n found   : _1.ctx.Tree where val _1: Helper\r\n required: Test.ctx.Tree\r\n  val tree : ctx.Tree  =  new Helper(ctx).f(5)\r\n```\r\n\r\nThe fact that classes in Scala are ignorant of _referential equality_ also\r\nlimits the expressive power of _dependent function types_. For example, given\r\nthe code below, currently it's impossible to implement the function `f`:\r\n\r\n```Scala\r\nclass Animal(name: String)\r\n\r\ntrait Foo[T]\r\nclass Bar(val a: Animal) extends Foo[a.type]\r\n\r\nval f : (a: Animal) => Foo[a.type] = ???\r\n```\r\n\r\nIf we try to implement `f` with `(a: Animal) =>  new Bar(a)`, the Dotty compiler will\r\ngenerate following error message:\r\n\r\n```Scala\r\n7 |  val f : (a: Animal) => Foo[a.type] = (a: Animal) =>  new Bar(a)\r\n  |                                                           ^^^^^\r\n  |                                                  found:    Bar\r\n  |                                                  required: Foo[Animal(a)]\r\n```\r\n\r\nBut the definition of `Bar` says that any instance of `Bar(a)` is a subtype of `Foo[a.type]`!\r\n\r\nRelated issues: https://github.com/scala/bug/issues/5712, https://github.com/scala/bug/issues/5700, #1262.\r\n\r\n## Proposal\r\n\r\nTo address the problems above as well as make dependent types more useful, we\r\npropose _dependent class types_. We introduce an annotation `@dependent` that can be\r\nused to mark a public field of in a class constructor depenent:\r\n\r\n```Scala\r\nclass Animal(name: String)\r\n\r\ntrait Foo[T]\r\nclass Bar(@dependent val a: Animal) extends Foo[a.type]\r\n```\r\n\r\nThe compiler should produce a _dependent refinement type_ for dependent class instantiation as follows:\r\n\r\n``` Scala\r\nval dog  : Dog =  new Animal(\"dog\")\r\nval bar  : Bar { val a: dog.type @dependent }  =  new Bar(dog)\r\n```\r\n\r\nThe subtype checking should allow the following:\r\n\r\n```Scala\r\n// Bar { val a: dog.type @dependent }  <:  Foo[dog.type]\r\nval foo  : Foo[dog.type] = bar\r\n```\r\n\r\n## Rules\r\n\r\n1. `@dependent` can only be used in class primary constructor to decorate\r\n   _non-private_, _non-mutable_, _non-lazy_, _non-overloaded_ fields.\r\n\r\n2. A depenent refinement type  `M { val x: T @dependent }` is valid if `x` is a\r\n   _non-private_, _non-mutable_, _non-lazy_, _non-overloaded_ field of `M`, and\r\n   `T` is a subtype of `M.member(x)`.\r\n\r\n3. If a primary constructor parameter `x` of a class `Bar` is annotated with\r\n   `@dependent`, the return type of the constructor is refined as `Bar { val x: x.type\r\n   @dependent }`. The `x` in `x.type` refers the constructor parameter, thus the constructor\r\n   has a dependent method type.\r\n\r\n4. When getting the base type of a _valid_ dependent refinement type `M { val x:\r\n   T @dependent }` for a parent class `P`,  first get the base type `B` from\r\n   `baseType(M, P)`, then substitute all references to `M.member(x)` with the\r\n   type `T`.\r\n\r\n## Implementation\r\n\r\nWe don't need syntax change to the language, nor introduce new types in the compiler.\r\n\r\n1. We need to introduce an annotation `@dependent`.\r\n\r\n```Scala\r\npackage scala.annotation\r\n\r\nfinal class dependent extends StaticAnnotation\r\n```\r\n\r\n2. We need add checks for valid usage of `@dependent` in class definitions and dependent refinement types. The checks are better to be done in RefChecks, as they are semantic.\r\n\r\n3. We need to update the type checking for constructors, to refine the result type with the dependent refinement `{ val x: x.type @dependent }` if any constructor parameter `x` is annotated with `@dependent`. The change in consideration looks like the following:\r\n\r\n```Scala\r\nval oldRetType  = ...\r\nval refinedRetType = termParamss.foldLeft(oldRetType) { (acc, termParams) =>\r\n  termParams.foldLeft(acc) { (acc, termParam) =>\r\n    if (acc.hasDependentAnnotation)\r\n      RefinedType(acc, termParam.name, termParam.termRef)\r\n    else acc\r\n  }\r\n}\r\n```\r\n\r\n4. We need to change base type computation to handle dependent refinements. The change in consideration looks like the following:\r\n\r\n```Scala\r\ncase tp @ RefinedType(parent, name, refine) =>\r\n  val res = baseTypeOf(tp.superType)\r\n  if (tp.isDependentRefinement)\r\n    res.subst(tp.nonPrivateMember(name).symbol :: Nil, refine :: Nil)\r\n  else res\r\n```\r\n\r\n## Application\r\n\r\nDependent class types can implement ML-like functor modules:\r\n\r\n```Scala\r\nimport scala.annotation.dependent\r\n\r\ntrait Ordering {\r\n  type T\r\n  def compare(t1:T, t2: T): Int\r\n}\r\n\r\nclass SetFunctor(@dependent val ord: Ordering) {\r\n  type Set = List[ord.T]\r\n  def empty: Set = Nil\r\n\r\n  implicit class helper(s: Set) {\r\n    def add(x: ord.T): Set = x :: remove(x)\r\n    def remove(x: ord.T): Set = s.filter(e => ord.compare(x, e) != 0)\r\n    def member(x: ord.T): Boolean = s.exists(e => ord.compare(x, e) == 0)\r\n  }\r\n}\r\n\r\nobject Test {\r\n  val orderInt = new Ordering {\r\n    type T = Int\r\n    def compare(t1: T, t2: T): Int = t1 - t2\r\n  }\r\n\r\n  val IntSet = new SetFunctor(orderInt)\r\n  import IntSet._\r\n\r\n  def main(args: Array[String]) = {\r\n    val set = IntSet.empty.add(6).add(8).add(23)\r\n    assert(!set.member(7))\r\n    assert(set.member(8))\r\n  }\r\n}\r\n```\r\n\r\n## Change Logs\r\n\r\n1. Changed `@dep` to `@dependent`, thanks @propensive .\r\n2. Added related issues, thanks @julienrf .\r\n3. Add application about functor modules"},"comment":{"url":"https://api.github.com/repos/lampepfl/dotty/issues/comments/362902998","html_url":"https://github.com/lampepfl/dotty/issues/3920#issuecomment-362902998","issue_url":"https://api.github.com/repos/lampepfl/dotty/issues/3920","id":362902998,"user":{"login":"mdedetrich","id":2337269,"avatar_url":"https://avatars0.githubusercontent.com/u/2337269?v=4","gravatar_id":"","url":"https://api.github.com/users/mdedetrich","html_url":"https://github.com/mdedetrich","followers_url":"https://api.github.com/users/mdedetrich/followers","following_url":"https://api.github.com/users/mdedetrich/following{/other_user}","gists_url":"https://api.github.com/users/mdedetrich/gists{/gist_id}","starred_url":"https://api.github.com/users/mdedetrich/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mdedetrich/subscriptions","organizations_url":"https://api.github.com/users/mdedetrich/orgs","repos_url":"https://api.github.com/users/mdedetrich/repos","events_url":"https://api.github.com/users/mdedetrich/events{/privacy}","received_events_url":"https://api.github.com/users/mdedetrich/received_events","type":"User","site_admin":false},"created_at":"2018-02-04T12:26:09Z","updated_at":"2018-02-04T12:26:09Z","author_association":"NONE","body":"I actually really like the proposal said here https://github.com/lampepfl/dotty/issues/3920#issuecomment-361248494 with the caveat that `@dependant` should not be an annotation and it instead should be an actual keyword (i.e. `dependant`)\r\n\r\nI agree with @Blaisorblade  here though, both tickets are now closed which implies that none of the approaches are being considered?"}}
{"actor":{"display_login":"mdedetrich"}}