Skip to content

Commit a2bcf82

Browse files
committed
clear up points
1 parent 1d22fac commit a2bcf82

File tree

1 file changed

+54
-2
lines changed

1 file changed

+54
-2
lines changed

copy/entries/faking-adts-and-gadts.md

+54-2
Original file line numberDiff line numberDiff line change
@@ -932,6 +932,37 @@ In many languages, using this technique effectively requires having a newtype
932932
wrapper on-hand, so it might be unwieldy in non-trivial situations. But it can
933933
be a pretty powerful method for reasons we will see soon.
934934

935+
For example, if we wanted to write our previous axis function which is `NType a
936+
-> [a] -> String`, we'd have to have a newtype wrapper for `[a] -> String` that
937+
has `a` as its argument:
938+
939+
```purescript
940+
newtype OpList b a = Op ([a] -> b)
941+
```
942+
943+
or you could re-use `Compose`:
944+
945+
```purescript
946+
newtype Compose f g a = Compose (f (g a))
947+
```
948+
949+
and your `p` projection type would be `Compose Op []`. So, you don't
950+
necessarily have to write a bespoke newtype wrapper, _but_ you do have to
951+
devote some brain cycles to think it through (unless you're in a language
952+
that doesn't need newtype wrappers to have this work, like we'll discuss
953+
later).
954+
955+
By the way, this method generalizes well to multiple arguments: if you have a
956+
type like `MyGADT a b c`, you just need to project into a `forall (p :: k1 ->
957+
k2 -> k3 -> Type)`.
958+
959+
I believe I have read somewhere that the two methods here (runtime equality
960+
witness vs. higher-kinded eliminator) are not actually fully identical with
961+
each other, and there are GADTs where one would work and not the other ... but
962+
I can't remember where I read this and I'm also not big-brained enough to
963+
figure out what those situations are. But if you, reader, have any idea, please
964+
let me know!
965+
935966
### Existential Types
936967

937968
Let's take a quick break to talk about something that's not _technically_
@@ -993,8 +1024,7 @@ interface SomeNTypeVisitor<R> {
9931024
interface SomeNType {
9941025
public abstract <R> R accept(SomeNTypeVisitor<R> visitor);
9951026

996-
// use a factory method here, or a generic subclass with NType<A> and A
997-
// fields would work too
1027+
// One option: the factory method
9981028
public static <A> SomeNType someNType(NType<A> nt, A val) {
9991029
return new SomeNType() {
10001030
@Override
@@ -1004,6 +1034,22 @@ interface SomeNType {
10041034
};
10051035
}
10061036
}
1037+
1038+
// Second option: the subtype hiding a type variable
1039+
class SomeNTypeImpl<A> extends SomeNType {
1040+
private NType<A> nt;
1041+
private A val;
1042+
1043+
public SomeNTypeImpl(NType<A> nt, A val) {
1044+
this.nt = nt;
1045+
this.val = val;
1046+
}
1047+
1048+
@Override
1049+
public <R> R accept(SomeNTypeVisitor<R> visitor) {
1050+
return visitor.visit(nt, val);
1051+
}
1052+
}
10071053
```
10081054

10091055
Does...anyone write java like this? I tried committing this once while at
@@ -1158,6 +1204,12 @@ ternary :: Expr Bool -> Expr a -> Expr a -> Expr a
11581204
ternary b x y handlers = handlers.ternary (b handlers) (x handlers) (y handlers)
11591205
```
11601206

1207+
One nice thing about the dhall version that's incidental to dhall is that it
1208+
doesn't require any extra newtype wrappers like the Haskell one does. That's
1209+
because type inference tends to choke on things like this, but dhall doesn't
1210+
really have any type inference: all of the types are passed explicitly. It's
1211+
one of the facts about dhall that make it nice for things like this.
1212+
11611213
Congratulations
11621214
---------------
11631215

0 commit comments

Comments
 (0)