aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/library/lux/type/quotient.lux
blob: 5033db2a06cde202ff5e05c4b6137770926774da (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
(.module:
  [library
   [lux {"-" [type]}
    [abstract
     [equivalence {"+" [Equivalence]}]]
    [control
     [parser
      ["<.>" code]]]
    [macro {"+" [with_identifiers]}
     [syntax {"+" [syntax:]}]]
    ["." type
     abstract]]])

(abstract: .public (Class t c %)
  {}
  
  (-> t c)

  (def: .public class
    (All (_ t c)
      (Ex (_ %)
        (-> (-> t c) (Class t c %))))
    (|>> :abstraction))

  (abstract: .public (Quotient t c %)
    {}
    
    (Record
     [#value t
      #label c])

    (def: .public (quotient class value)
      (All (_ t c %)
        (-> (Class t c %) t
            (Quotient t c %)))
      (:abstraction [#value value
                     #label ((:representation Class class) value)]))

    (template [<name> <output> <slot>]
      [(def: .public <name>
         (All (_ t c %) (-> (Quotient t c %) <output>))
         (|>> :representation (value@ <slot>)))]

      [value t #value]
      [label c #label]
      )
    )
  )

(syntax: .public (type [class <code>.any])
  (with_identifiers [g!t g!c g!%]
    (in (list (` ((~! type.:by_example)
                  [(~ g!t) (~ g!c) (~ g!%)]

                  (..Class (~ g!t) (~ g!c) (~ g!%))
                  (~ class)
                  
                  (..Quotient (~ g!t) (~ g!c) (~ g!%))))))))

(implementation: .public (equivalence super)
  (All (_ t c %) (-> (Equivalence c) (Equivalence (..Quotient t c %))))

  (def: (= reference sample)
    (\ super = (..label reference) (..label sample))))