-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathmorph.knot
More file actions
52 lines (49 loc) · 2.22 KB
/
Copy pathmorph.knot
File metadata and controls
52 lines (49 loc) · 2.22 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
-- Type-directed conversion via record dictionaries + `^into` projection.
--
-- Conversions live under a single `morph` namespace, keyed by source then
-- target type: `morph.<from-type>.<to-type>.into` holds a function `S -> T`.
-- `(^into) x` resolves TYPE-DIRECTEDLY against the in-scope `into` fields:
--
-- * by the ARGUMENT type — when only one morph's `into` accepts x's type
-- (the resolver collects every same-depth `into`, then keeps the one
-- whose parameter type matches x);
--
-- * by the EXPECTED RESULT type — when the surrounding context demands a
-- concrete type (e.g. an annotation `v : Float 1 = (^into) x`), so two
-- morphs sharing x's source type (`text.int` vs `text.float`) are
-- disambiguated by which one produces the required target. This is the
-- bidirectional (check-mode) path: the contextual expected type threads
-- through the enclosing `with` into the application's result.
with {
textToInt { into : Text -> Int 1
into (\s -> base.length s) }
intToText { into : Int 1 -> Text
into (\n -> base.show n) }
textToFloat { into : Text -> Float 1
into (\s -> 2.5) }
-- The ambient conversion scope: base.morph.<from-type>.<to-type>.into
conv { morph {
text { int { into textToInt.into }
float { into textToFloat.into } }
int { text { into intToText.into } }
} }
-- Argument-type-directed: distinct source types. (These are annotated too,
-- because `text.int` and `text.float` below share the Text source — an
-- un-annotated Text `into` would be ambiguous. The annotation is what lets
-- the result type pick.)
argInt : Int 1
argInt (with conv ((^into) "hi")) -- Text arg, wants Int 1
argText : Text
argText (with conv ((^into) 41)) -- Int arg, wants Text
-- Result-type-directed: same source (Text), annotation picks the target.
asInt : Int 1
asInt (with conv ((^into) "hi")) -- wants Int 1 -> morph.text.int.into
asFloat : Float 1
asFloat (with conv ((^into) "hi")) -- wants Float 1 -> morph.text.float.into
}
(do
base.println (base.show argInt) -- "2" (length of "hi")
base.println (base.show argText) -- "41"
base.println (base.show asInt) -- "2"
base.println (base.show asFloat) -- "2.5"
yield {})