blob: 08346c47b833176dfaa4a8cc844beab3a01b9b6d (
plain)
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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
(.module:
[lux #*
[abstract ["." monad (#+ do)]]
[data
["%" text/format (#+ format)]
["." name ("#@." equivalence)]]
["r" math/random (#+ Random) ("#@." monad)]
["_" test (#+ Test)]
[control
pipe]
[data
["." error]
["." maybe]
["." product]
["." text ("#@." equivalence)]
[collection
["." list ("#@." functor)]]]
["." type]
["." macro
["." code]]]
[//
["_." primitive]
["_." structure]]
{1
["." /
["/#" //
["#." module]
["#." type]
["/#" //
["/#" //
["#." reference]
["#." analysis (#+ Analysis Operation)]]]]]})
(def: (check-apply expectedT num-args analysis)
(-> Type Nat (Operation Analysis) Bit)
(|> analysis
(//type.with-type expectedT)
(///.run _primitive.state)
(case> (#error.Success applyA)
(let [[funcA argsA] (////analysis.application applyA)]
(n/= num-args (list.size argsA)))
(#error.Failure error)
false)))
(def: abstraction
(do r.monad
[func-name (r.unicode 5)
arg-name (|> (r.unicode 5) (r.filter (|>> (text@= func-name) not)))
[outputT outputC] _primitive.primitive
[inputT _] _primitive.primitive
#let [g!arg (code.local-identifier arg-name)]]
(<| (_.context (%.name (name-of /.function)))
($_ _.and
(_.test "Can analyse function."
(and (|> (//type.with-type (All [a] (-> a outputT))
(/.function _primitive.phase func-name arg-name outputC))
_structure.check-succeeds)
(|> (//type.with-type (All [a] (-> a a))
(/.function _primitive.phase func-name arg-name g!arg))
_structure.check-succeeds)))
(_.test "Generic functions can always be specialized."
(and (|> (//type.with-type (-> inputT outputT)
(/.function _primitive.phase func-name arg-name outputC))
_structure.check-succeeds)
(|> (//type.with-type (-> inputT inputT)
(/.function _primitive.phase func-name arg-name g!arg))
_structure.check-succeeds)))
(_.test "The function's name is bound to the function's type."
(|> (//type.with-type (Rec self (-> inputT self))
(/.function _primitive.phase func-name arg-name (code.local-identifier func-name)))
_structure.check-succeeds))
))))
(def: apply
(do r.monad
[full-args (|> r.nat (:: @ map (|>> (n/% 10) (n/max 2))))
partial-args (|> r.nat (:: @ map (n/% full-args)))
var-idx (|> r.nat (:: @ map (|>> (n/% full-args) (n/max 1))))
inputsTC (r.list full-args _primitive.primitive)
#let [inputsT (list@map product.left inputsTC)
inputsC (list@map product.right inputsTC)]
[outputT outputC] _primitive.primitive
#let [funcT (type.function inputsT outputT)
partialT (type.function (list.drop partial-args inputsT) outputT)
varT (#.Parameter 1)
polyT (<| (type.univ-q 1)
(type.function (list.concat (list (list.take var-idx inputsT)
(list varT)
(list.drop (inc var-idx) inputsT))))
varT)
poly-inputT (maybe.assume (list.nth var-idx inputsT))
partial-poly-inputsT (list.drop (inc var-idx) inputsT)
partial-polyT1 (<| (type.function partial-poly-inputsT)
poly-inputT)
partial-polyT2 (<| (type.univ-q 1)
(type.function (#.Cons varT partial-poly-inputsT))
varT)
dummy-function (#////analysis.Function (list) (#////analysis.Reference (////reference.local 1)))]]
(<| (_.context (%.name (name-of /.apply)))
($_ _.and
(_.test "Can analyse monomorphic type application."
(|> (/.apply _primitive.phase funcT dummy-function (' []) inputsC)
(check-apply outputT full-args)))
(_.test "Can partially apply functions."
(|> (/.apply _primitive.phase funcT dummy-function (' []) (list.take partial-args inputsC))
(check-apply partialT partial-args)))
(_.test "Can apply polymorphic functions."
(|> (/.apply _primitive.phase polyT dummy-function (' []) inputsC)
(check-apply poly-inputT full-args)))
(_.test "Polymorphic partial application propagates found type-vars."
(|> (/.apply _primitive.phase polyT dummy-function (' []) (list.take (inc var-idx) inputsC))
(check-apply partial-polyT1 (inc var-idx))))
(_.test "Polymorphic partial application preserves quantification for type-vars."
(|> (/.apply _primitive.phase polyT dummy-function (' []) (list.take var-idx inputsC))
(check-apply partial-polyT2 var-idx)))
))))
(def: #export test
Test
(<| (_.context (name.module (name-of /._)))
($_ _.and
..abstraction
..apply
)))
|
