Skip to content

Commit 8b6ed58

Browse files
committed
fix gadts.md layout
1 parent 51b7d55 commit 8b6ed58

File tree

1 file changed

+26
-21
lines changed

1 file changed

+26
-21
lines changed

docs/_docs/internals/gadts.md

Lines changed: 26 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,9 @@
1-
# GADTs - Broad overview
1+
---
2+
layout: doc-page
3+
title: "GADTs - Broad overview"
4+
---
5+
6+
## Introduction
27

38
There are multiple levels to the implementation. They deal with slightly different problems. The most important levels are the following ones:
49

@@ -18,9 +23,9 @@ There are also other parts to supporting GADTs. Roughly in order of importance,
1823
1. Attachment key is named `inferredGadtConstraints`.
1924
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.
2025

21-
# Useful widgets
26+
## Useful widgets
2227

23-
## Expr
28+
### Expr
2429

2530
This is the classical GADT example:
2631

@@ -36,7 +41,7 @@ enum Expr[T] {
3641
}
3742
```
3843

39-
## EQ
44+
### EQ
4045

4146
The following enum will result in an equality constraint between `S` and `T` if we match on it:
4247

@@ -46,7 +51,7 @@ enum EQ[S, T] {
4651
}
4752
```
4853

49-
## SUB
54+
### SUB
5055

5156
The following enum will result in a subtyping constraint `S <: T` if we match on it:
5257

@@ -56,9 +61,9 @@ enum SUB[-S, +T] {
5661
}
5762
```
5863

59-
# Details of above
64+
## Details of above
6065

61-
## What abstract types can have GADT constraints
66+
### What abstract types can have GADT constraints
6267

6368
Right now, we record GADT constraints for:
6469

@@ -67,9 +72,9 @@ Right now, we record GADT constraints for:
6772

6873
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".
6974

70-
## What are necessary relationships? Any examples?
75+
### What are necessary relationships? Any examples?
7176

72-
### Covariance means no constraint is necessary
77+
#### Covariance means no constraint is necessary
7378

7479
Standard (non-case) classes allow "strange" inheritance which means that we cannot infer any information from covariant type parameters.
7580

@@ -90,7 +95,7 @@ class Weird(list: List[String]) extends IntList with Expr[Nothing]
9095

9196
Case classes have a special check which disallows inheritance like `Weird`. This means we can infer extra information from them.
9297

93-
## Breaking down the constraints
98+
### Breaking down the constraints
9499

95100
```scala
96101
class Expr[A]
@@ -113,9 +118,9 @@ def foo[T](e: Expr[List[T]]): T =
113118
}
114119
```
115120

116-
## Relation betweeen GadtConstraint and OrderingConstraint
121+
### Relation betweeen GadtConstraint and OrderingConstraint
117122

118-
### Internal and external types
123+
#### Internal and external types
119124

120125
GadtConstraint uses OrderingConstraint as the datastructure to record information about GADT constraints.
121126

@@ -127,9 +132,9 @@ To solve this, GadtConstraint internally creates TypeParamRefs which it adds to
127132

128133
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 &#x2013; we will always try to record bounds in the "normal" constraint before recording a GADT bound.)
129134

130-
# Other details
135+
## Other details
131136

132-
## TypeComparer approximations
137+
### TypeComparer approximations
133138

134139
TypeComparer sometimes approximates the types it compares. Let's see an example based on these definitions:
135140

@@ -142,11 +147,11 @@ when comparing if `IntList <: Expr[Int]`, `TypeComparer` will approximate `IntLi
142147

143148
The variables which TypeComparer sets are `approxState` and `frozenGadt`.
144149

145-
## Necessary/sufficient either
150+
### Necessary/sufficient either
146151

147152
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`.
148153

149-
## Types bound in patterns
154+
### Types bound in patterns
150155

151156
```scala
152157
(list : List[Int]) match {
@@ -161,7 +166,7 @@ TypeComparer sometimes needs to approximate some constraints, specifically when
161166
}
162167
```
163168

164-
## Internal structure of OrderingConstraint
169+
### Internal structure of OrderingConstraint
165170

166171
Imagine we have two type parameters in scope, `A` and `B`.
167172

@@ -184,19 +189,19 @@ B <: A
184189

185190
The first two constraints are "entries" &#x2013; they are easy to look up whenever we ask for bounds of `A` or `B`. The third constraint is an ordering &#x2013; it helps with correctly propagating the bounds we record.
186191

187-
# Possible broad improvements
192+
## Possible broad improvements
188193

189-
## Allow OrderingConstraint to record bounds for things other than TypeParamRefs
194+
### Allow OrderingConstraint to record bounds for things other than TypeParamRefs
190195

191196
This would mean we no longer need to keep the bidirectional mapping in GadtConstraint.
192197

193-
## Not mixing OrderingConstraint and ConstraintHandling in GadtConstraint
198+
### Not mixing OrderingConstraint and ConstraintHandling in GadtConstraint
194199

195200
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.
196201

197202
GadtConstraint mixes them both. Things would be better organised if GadtConstraint was split like the normal constraint.
198203

199-
## Creating a separate TypeComparer for breaking down types into GADT constraints
204+
### Creating a separate TypeComparer for breaking down types into GADT constraints
200205

201206
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.
202207

0 commit comments

Comments
 (0)