path: root/stdlib/source/library/lux/type.lux

(.module:
  {#.doc "Basic functionality for working with types."}
  [library
   [lux (#- function :as)
    ["@" target]
    [abstract
     [equivalence (#+ Equivalence)]
     [monad (#+ Monad do)]]
    [control
     ["." function]
     ["." maybe]
     ["." exception (#+ exception:)]
     ["<>" parser
      ["<.>" code (#+ Parser)]]]
    [data
     ["." product]
     ["." text ("#\." monoid equivalence)]
     ["." name ("#\." equivalence codec)]
     [collection
      ["." array]
      ["." list ("#\." functor monoid mix)]]]
    ["." macro
     [syntax (#+ syntax:)]
     ["." code]]
    [math
     [number
      ["n" nat ("#\." decimal)]]]
    ["." meta
     ["." location]]]])

(template [<name> <tag>]
  [(def: .public (<name> type)
     {#.doc (example "The number of parameters, and the body, of a quantified type.")}
     (-> Type [Nat Type])
     (loop [num_args 0
            type type]
       (case type
         (<tag> env sub_type)
         (recur (++ num_args) sub_type)

         _
         [num_args type])))]

  [flat_univ_q #.UnivQ]
  [flat_ex_q   #.ExQ]
  )

(def: .public (flat_function type)
  {#.doc (example "The input, and the output of a function type.")}
  (-> Type [(List Type) Type])
  (case type
    (#.Function in out')
    (let [[ins out] (flat_function out')]
      [(list& in ins) out])

    _
    [(list) type]))

(def: .public (flat_application type)
  {#.doc (example "The quantified type, and its parameters, for a type-application.")}
  (-> Type [Type (List Type)])
  (case type
    (#.Apply arg func')
    (let [[func args] (flat_application func')]
      [func (list\compose args (list arg))])

    _
    [type (list)]))

(template [<name> <tag>]
  [(def: .public (<name> type)
     {#.doc (example "The members of a composite type.")}
     (-> Type (List Type))
     (case type
       (<tag> left right)
       (list& left (<name> right))

       _
       (list type)))]

  [flat_variant #.Sum]
  [flat_tuple   #.Product]
  )

(def: .public (format type)
  {#.doc (example "A (readable) textual representable of a type.")}
  (-> Type Text)
  (case type
    (#.Primitive name params)
    ($_ text\compose
        "(primitive "
        (text.enclosed' text.double_quote name)
        (|> params
            (list\map (|>> format (text\compose " ")))
            (list\mix (function.flipped text\compose) ""))
        ")")

    (^template [<tag> <open> <close> <flat>]
      [(<tag> _)
       ($_ text\compose <open>
           (|> (<flat> type)
               (list\map format)
               list.reversed
               (list.interposed " ")
               (list\mix text\compose ""))
           <close>)])
    ([#.Sum  "(Or " ")" flat_variant]
     [#.Product "["   "]" flat_tuple])

    (#.Function input output)
    (let [[ins out] (flat_function type)]
      ($_ text\compose  "(-> "
          (|> ins
              (list\map format)
              list.reversed
              (list.interposed " ")
              (list\mix text\compose ""))
          " " (format out) ")"))

    (#.Parameter idx)
    (n\encoded idx)

    (#.Var id)
    ($_ text\compose "⌈v:" (n\encoded id) "⌋")

    (#.Ex id)
    ($_ text\compose "⟨e:" (n\encoded id) "⟩")

    (#.Apply param fun)
    (let [[type_func type_args] (flat_application type)]
      ($_ text\compose  "(" (format type_func) " " (|> type_args (list\map format) list.reversed (list.interposed " ") (list\mix text\compose "")) ")"))

    (^template [<tag> <desc>]
      [(<tag> env body)
       ($_ text\compose "(" <desc> " {" (|> env (list\map format) (text.interposed " ")) "} " (format body) ")")])
    ([#.UnivQ "All"]
     [#.ExQ "Ex"])

    (#.Named [module name] type)
    ($_ text\compose module "." name)
    ))

... https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction
(def: (reduced env type)
  (-> (List Type) Type Type)
  (case type
    (#.Primitive name params)
    (#.Primitive name (list\map (reduced env) params))
    
    (^template [<tag>]
      [(<tag> left right)
       (<tag> (reduced env left) (reduced env right))])
    ([#.Sum]      [#.Product]
     [#.Function] [#.Apply])
    
    (^template [<tag>]
      [(<tag> old_env def)
       (case old_env
         #.End
         (<tag> env def)

         _
         (<tag> (list\map (reduced env) old_env) def))])
    ([#.UnivQ]
     [#.ExQ])
    
    (#.Parameter idx)
    (maybe.else (panic! ($_ text\compose
                            "Unknown type parameter" text.new_line
                            "      Index: " (n\encoded idx) text.new_line
                            "Environment: " (|> env
                                                list.enumeration
                                                (list\map (.function (_ [index type])
                                                            ($_ text\compose
                                                                (n\encoded index)
                                                                " " (..format type))))
                                                (text.interposed (text\compose text.new_line "             ")))))
                (list.item idx env))
    
    _
    type
    ))

(implementation: .public equivalence
  (Equivalence Type)
  
  (def: (= x y)
    (or (for {@.php false} ... TODO: Remove this once JPHP is gone.
             (same? x y))
        (case [x y]
          [(#.Primitive xname xparams) (#.Primitive yname yparams)]
          (and (text\= xname yname)
               (n.= (list.size yparams) (list.size xparams))
               (list\mix (.function (_ [x y] prev) (and prev (= x y)))
                         #1
                         (list.zipped/2 xparams yparams)))

          (^template [<tag>]
            [[(<tag> xid) (<tag> yid)]
             (n.= yid xid)])
          ([#.Var] [#.Ex] [#.Parameter])

          (^or [(#.Function xleft xright) (#.Function yleft yright)]
               [(#.Apply xleft xright) (#.Apply yleft yright)])
          (and (= xleft yleft)
               (= xright yright))

          [(#.Named xname xtype) (#.Named yname ytype)]
          (and (name\= xname yname)
               (= xtype ytype))

          (^template [<tag>]
            [[(<tag> xL xR) (<tag> yL yR)]
             (and (= xL yL) (= xR yR))])
          ([#.Sum] [#.Product])
          
          (^or [(#.UnivQ xenv xbody) (#.UnivQ yenv ybody)]
               [(#.ExQ xenv xbody) (#.ExQ yenv ybody)])
          (and (n.= (list.size yenv) (list.size xenv))
               (= xbody ybody)
               (list\mix (.function (_ [x y] prev) (and prev (= x y)))
                         #1
                         (list.zipped/2 xenv yenv)))

          _
          #0
          ))))

(def: .public (applied params func)
  {#.doc (example "To the extend possible, applies a quantified type to the given parameters.")}
  (-> (List Type) Type (Maybe Type))
  (case params
    #.End
    (#.Some func)

    (#.Item param params')
    (case func
      (^template [<tag>]
        [(<tag> env body)
         (|> body
             (reduced (list& func param env))
             (applied params'))])
      ([#.UnivQ] [#.ExQ])

      (#.Apply A F)
      (applied (list& A params) F)

      (#.Named name unnamed)
      (applied params unnamed)
      
      _
      #.None)))

(def: .public (code type)
  {#.doc (example "A representation of a type as code."
                  "The code is such that evaluating it would yield the type value.")}
  (-> Type Code)
  (case type
    (#.Primitive name params)
    (` (#.Primitive (~ (code.text name))
                    (.list (~+ (list\map code params)))))

    (^template [<tag>]
      [(<tag> idx)
       (` (<tag> (~ (code.nat idx))))])
    ([#.Var] [#.Ex] [#.Parameter])

    (^template [<tag>]
      [(<tag> left right)
       (` (<tag> (~ (code left))
                 (~ (code right))))])
    ([#.Sum] [#.Product] [#.Function] [#.Apply])

    (#.Named name sub_type)
    (code.identifier name)

    (^template [<tag>]
      [(<tag> env body)
       (` (<tag> (.list (~+ (list\map code env)))
                 (~ (code body))))])
    ([#.UnivQ] [#.ExQ])
    ))

(def: .public (de_aliased type)
  {#.doc (example "A (potentially named) type that does not have its name shadowed by other names.")}
  (-> Type Type)
  (case type
    (#.Named _ (#.Named name type'))
    (de_aliased (#.Named name type'))

    _
    type))

(def: .public (anonymous type)
  {#.doc (example "A type without any names covering it.")}
  (-> Type Type)
  (case type
    (#.Named name type')
    (anonymous type')

    _
    type))

(template [<name> <base> <ctor>]
  [(def: .public (<name> types)
     {#.doc (example "A composite type, constituted by the given member types.")}
     (-> (List Type) Type)
     (case types
       #.End
       <base>

       (#.Item type #.End)
       type

       (#.Item type types')
       (<ctor> type (<name> types'))))]

  [variant Nothing #.Sum]
  [tuple   Any     #.Product]
  )

(def: .public (function inputs output)
  {#.doc (example "A function type, with the given inputs and output.")}
  (-> (List Type) Type Type)
  (case inputs
    #.End
    output

    (#.Item input inputs')
    (#.Function input (function inputs' output))))

(def: .public (application params quant)
  {#.doc (example "An un-evaluated type application, with the given quantified type, and parameters.")}
  (-> (List Type) Type Type)
  (case params
    #.End
    quant

    (#.Item param params')
    (application params' (#.Apply param quant))))

(template [<name> <tag>]
  [(def: .public (<name> size body)
     {#.doc (example "A quantified type, with the given number of parameters, and body.")}
     (-> Nat Type Type)
     (case size
       0 body
       _  (|> body (<name> (-- size)) (<tag> (list)))))]

  [univ_q #.UnivQ]
  [ex_q   #.ExQ]
  )

(def: .public (quantified? type)
  {#.doc (example "Only yields #1 for universally or existentially quantified types.")}
  (-> Type Bit)
  (case type
    (#.Named [module name] _type)
    (quantified? _type)

    (#.Apply A F)
    (|> (..applied (list A) F)
        (\ maybe.monad map quantified?)
        (maybe.else #0))
    
    (^or (#.UnivQ _) (#.ExQ _))
    #1

    _
    #0))

(def: .public (array depth element_type)
  {#.doc (example "An array type, with the given level of nesting/depth, and the given element type.")}
  (-> Nat Type Type)
  (case depth
    0 element_type
    _ (|> element_type
          (array (-- depth))
          (list)
          (#.Primitive array.type_name))))

(def: .public (flat_array type)
  {#.doc (example "The level of nesting/depth and element type for an array type.")}
  (-> Type [Nat Type])
  (case type
    (^multi (^ (#.Primitive name (list element_type)))
            (text\= array.type_name name))
    (let [[depth element_type] (flat_array element_type)]
      [(++ depth) element_type])

    _
    [0 type]))

(def: .public array?
  {#.doc (example "Is a type an array type?")}
  (-> Type Bit)
  (|>> ..flat_array
       product.left
       (n.> 0)))

(syntax: (new_secret_marker [])
  (macro.with_identifiers [g!_secret_marker_]
    (in (list g!_secret_marker_))))

(def: secret_marker
  (`` (name_of (~~ (new_secret_marker)))))

(syntax: .public (:log! [input (<>.or (<>.and <code>.identifier
                                              (<>.maybe (<>.after (<code>.identifier! ..secret_marker) <code>.any)))
                                      <code>.any)])
  {#.doc (example "Logs to the console/terminal the type of an expression."
                  (:log! (: Foo (foo expression)))
                  "=>"
                  "Expression: (foo expression)"
                  "      Type: Foo"
                  (foo expression))}
  (case input
    (#.Left [valueN valueC])
    (do meta.monad
      [location meta.location
       valueT (meta.type valueN)
       .let [_ ("lux io log"
                ($_ text\compose
                    (name\encoded (name_of ..:log!)) " " (location.format location) text.new_line
                    "Expression: " (case valueC
                                     (#.Some valueC)
                                     (code.format valueC)
                                     
                                     #.None
                                     (name\encoded valueN))
                    text.new_line
                    "      Type: " (..format valueT)))]]
      (in (list (code.identifier valueN))))
    
    (#.Right valueC)
    (macro.with_identifiers [g!value]
      (in (list (` (.let [(~ g!value) (~ valueC)]
                     (..:log! (~ valueC) (~ (code.identifier ..secret_marker)) (~ g!value)))))))))

(def: type_parameters
  (Parser (List Text))
  (<code>.tuple (<>.some <code>.local_identifier)))

(syntax: .public (:as [type_vars type_parameters
                       input <code>.any
                       output <code>.any
                       value (<>.maybe <code>.any)])
  {#.doc (example "Casts a value to a specific type."
                  "The specified type can depend on type variables of the original type of the value."
                  (: (Bar Bit Nat Text)
                     (:as [a b c]
                          (Foo a [b c])
                          (Bar a b c)
                          (: (Foo Bit [Nat Text])
                             (foo expression))))
                  "NOTE: Careless use of type-casts is an easy way to introduce bugs. USE WITH CAUTION.")}
  (let [casterC (` (: (All [(~+ (list\map code.local_identifier type_vars))]
                        (-> (~ input) (~ output)))
                      (|>> :expected)))]
    (case value
      #.None
      (in (list casterC))
      
      (#.Some value)
      (in (list (` ((~ casterC) (~ value))))))))

(type: Typed
  {#type Code
   #expression Code})

(def: typed
  (Parser Typed)
  (<>.and <code>.any <code>.any))

... TODO: Make sure the generated code always gets optimized away.
(syntax: .public (:sharing [type_vars ..type_parameters
                            exemplar ..typed
                            computation ..typed])
  {#.doc (example "Allows specifing the type of an expression as sharing type-variables with the type of another expression."
                  (: (Bar Bit Nat Text)
                     (:sharing [a b c]
                               (Foo a [b c])
                               (: (Foo Bit [Nat Text])
                                  (foo expression))
                               
                               (Bar a b c)
                               (bar expression))))}
  (macro.with_identifiers [g!_]
    (let [shareC (` (: (All [(~+ (list\map code.local_identifier type_vars))]
                         (-> (~ (value@ #type exemplar))
                             (~ (value@ #type computation))))
                       (.function ((~ g!_) (~ g!_))
                         (~ (value@ #expression computation)))))]
      (in (list (` ((~ shareC) (~ (value@ #expression exemplar)))))))))

(syntax: .public (:by_example [type_vars ..type_parameters
                               exemplar ..typed
                               extraction <code>.any])
  {#.doc (example "Constructs a type that shares type-variables with an expression of some other type."
                  (: Type
                     (:by_example [a b c]
                                  (Foo a [b c])
                                  (: (Foo Bit [Nat Text])
                                     (foo expression))
                                  
                                  (Bar a b c)))
                  "=>"
                  (.type (Bar Bit Nat Text)))}
  (in (list (` (:of ((~! :sharing)
                     [(~+ (list\map code.local_identifier type_vars))]

                     (~ (value@ #type exemplar))
                     (~ (value@ #expression exemplar))
                     
                     (~ extraction)
                     (:expected [])))))))