You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs/_docs/internals/gadts.md
+26-21
Original file line number
Diff line number
Diff line change
@@ -1,4 +1,9 @@
1
-
# GADTs - Broad overview
1
+
---
2
+
layout: doc-page
3
+
title: "GADTs - Broad overview"
4
+
---
5
+
6
+
## Introduction
2
7
3
8
There are multiple levels to the implementation. They deal with slightly different problems. The most important levels are the following ones:
4
9
@@ -18,9 +23,9 @@ There are also other parts to supporting GADTs. Roughly in order of importance,
18
23
1. Attachment key is named `inferredGadtConstraints`.
19
24
4. When we select members on a type that may have GADT constraints, we perform special "healing" by approximating the type using those constraints. We cannot take the constraints into account because member lookup is cached, and GADT constraints are only valid for specific scopes.
20
25
21
-
# Useful widgets
26
+
##Useful widgets
22
27
23
-
## Expr
28
+
###Expr
24
29
25
30
This is the classical GADT example:
26
31
@@ -36,7 +41,7 @@ enum Expr[T] {
36
41
}
37
42
```
38
43
39
-
## EQ
44
+
###EQ
40
45
41
46
The following enum will result in an equality constraint between `S` and `T` if we match on it:
42
47
@@ -46,7 +51,7 @@ enum EQ[S, T] {
46
51
}
47
52
```
48
53
49
-
## SUB
54
+
###SUB
50
55
51
56
The following enum will result in a subtyping constraint `S <: T` if we match on it:
52
57
@@ -56,9 +61,9 @@ enum SUB[-S, +T] {
56
61
}
57
62
```
58
63
59
-
# Details of above
64
+
##Details of above
60
65
61
-
## What abstract types can have GADT constraints
66
+
###What abstract types can have GADT constraints
62
67
63
68
Right now, we record GADT constraints for:
64
69
@@ -67,9 +72,9 @@ Right now, we record GADT constraints for:
67
72
68
73
There is a branch on the way which will also record them for type members (so path-dependent types) and singleton types. It has a paper associated: "Implementing path-depepdent GADTs for Scala 3".
69
74
70
-
## What are necessary relationships? Any examples?
75
+
###What are necessary relationships? Any examples?
71
76
72
-
### Covariance means no constraint is necessary
77
+
####Covariance means no constraint is necessary
73
78
74
79
Standard (non-case) classes allow "strange" inheritance which means that we cannot infer any information from covariant type parameters.
75
80
@@ -90,7 +95,7 @@ class Weird(list: List[String]) extends IntList with Expr[Nothing]
90
95
91
96
Case classes have a special check which disallows inheritance like `Weird`. This means we can infer extra information from them.
92
97
93
-
## Breaking down the constraints
98
+
###Breaking down the constraints
94
99
95
100
```scala
96
101
classExpr[A]
@@ -113,9 +118,9 @@ def foo[T](e: Expr[List[T]]): T =
113
118
}
114
119
```
115
120
116
-
## Relation betweeen GadtConstraint and OrderingConstraint
121
+
###Relation betweeen GadtConstraint and OrderingConstraint
117
122
118
-
### Internal and external types
123
+
####Internal and external types
119
124
120
125
GadtConstraint uses OrderingConstraint as the datastructure to record information about GADT constraints.
121
126
@@ -127,9 +132,9 @@ To solve this, GadtConstraint internally creates TypeParamRefs which it adds to
127
132
128
133
The TypeParamRefs and TypeVars registered in one constraint cannot ever be present in types mentioned in the other type constraint. The internal TypeParamRefs and TypeVars cannot ever leak out of the GadtConstraint. We cannot ever record a bound in GadtConstraint which mentions TypeParamRefs used for type inference. (That part is ensured by the way TypeComparer is organised – we will always try to record bounds in the "normal" constraint before recording a GADT bound.)
129
134
130
-
# Other details
135
+
##Other details
131
136
132
-
## TypeComparer approximations
137
+
###TypeComparer approximations
133
138
134
139
TypeComparer sometimes approximates the types it compares. Let's see an example based on these definitions:
135
140
@@ -142,11 +147,11 @@ when comparing if `IntList <: Expr[Int]`, `TypeComparer` will approximate `IntLi
142
147
143
148
The variables which TypeComparer sets are `approxState` and `frozenGadt`.
144
149
145
-
## Necessary/sufficient either
150
+
###Necessary/sufficient either
146
151
147
152
TypeComparer sometimes needs to approximate some constraints, specifically when dealing with intersection and union types. The way this approximation works changes if we're currently inferring GADT constraints. This is hopefully documented well in TypeComparer in doc comments for `necessaryEither` and `sufficientEither`.
148
153
149
-
## Types bound in patterns
154
+
###Types bound in patterns
150
155
151
156
```scala
152
157
(list : List[Int]) match {
@@ -161,7 +166,7 @@ TypeComparer sometimes needs to approximate some constraints, specifically when
161
166
}
162
167
```
163
168
164
-
## Internal structure of OrderingConstraint
169
+
###Internal structure of OrderingConstraint
165
170
166
171
Imagine we have two type parameters in scope, `A` and `B`.
167
172
@@ -184,19 +189,19 @@ B <: A
184
189
185
190
The first two constraints are "entries" – they are easy to look up whenever we ask for bounds of `A` or `B`. The third constraint is an ordering – it helps with correctly propagating the bounds we record.
186
191
187
-
# Possible broad improvements
192
+
##Possible broad improvements
188
193
189
-
## Allow OrderingConstraint to record bounds for things other than TypeParamRefs
194
+
###Allow OrderingConstraint to record bounds for things other than TypeParamRefs
190
195
191
196
This would mean we no longer need to keep the bidirectional mapping in GadtConstraint.
192
197
193
-
## Not mixing OrderingConstraint and ConstraintHandling in GadtConstraint
198
+
###Not mixing OrderingConstraint and ConstraintHandling in GadtConstraint
194
199
195
200
GadtConstraint right now mixes OrderingConstraint and ConstraintHandling. The first one is supposed to be the immutable constraint datastructure. The second one implements mutable functionality around a variable containing the immutable datastructure.
196
201
197
202
GadtConstraint mixes them both. Things would be better organised if GadtConstraint was split like the normal constraint.
198
203
199
-
## Creating a separate TypeComparer for breaking down types into GADT constraints
204
+
###Creating a separate TypeComparer for breaking down types into GADT constraints
200
205
201
206
TypeComparer is biased towards one specific way of approximating constraints. When we infer types, it's ok to be "optimistic". When inferring GADT constraints, we should be as pessimistic as possible, in order to only infer constraints which are necessary.
Copy file name to clipboardExpand all lines: docs/_docs/reference/contextual/derivation.md
+2-2
Original file line number
Diff line number
Diff line change
@@ -284,7 +284,7 @@ Note the following properties of `Mirror` types,
284
284
+ The methods `ordinal` and `fromProduct` are defined in terms of `MirroredMonoType` which is the type of kind-`*`
285
285
which is obtained from `MirroredType` by wildcarding its type parameters.
286
286
287
-
###Implementing `derived` with `Mirror`
287
+
## Implementing `derived` with `Mirror`
288
288
289
289
As seen before, the signature and implementation of a `derived` method for a type class `TC[_]` are arbitrary, but we expect it to typically be of the following form:
290
290
@@ -484,7 +484,7 @@ The framework described here enables all three of these approaches without manda
484
484
For a brief discussion on how to use macros to write a type class `derived`
485
485
method please read more at [How to write a type class `derived` method using macros](./derivation-macro.md).
Copy file name to clipboardExpand all lines: docs/_docs/reference/other-new-features/opaques.md
+1-1
Original file line number
Diff line number
Diff line change
@@ -174,6 +174,6 @@ val z = l2(3.1)
174
174
l1.mul(x, y) // type checks
175
175
l1.mul(x, z) // error: found l2.Logarithm, required l1.Logarithm
176
176
```
177
-
In general, one can think of an opaque type as being only transparent in the scope of `private[this]`.
177
+
In general, one can think of an opaque type as being only transparent in the scope of `private[this]` (unless the type is a top level definition - in this case, it's transparent only within the file it's defined in).
0 commit comments