(.using
  [library
   [lux {"-" function :as}
    ["$" documentation {"+" documentation:}]
    [control
     ["<>" parser
      ["<[0]>" code]]]
    [data
     ["[0]" text {"+" \n}
      ["%" format]]]
    [macro
     ["[0]" template]]]]
  [\\library
   ["[0]" /]]
  ["[0]" / "_"
   ["[1][0]" abstract]
   ["[1][0]" check]
   ["[1][0]" dynamic]
   ["[1][0]" implicit]
   ["[1][0]" poly]
   ["[1][0]" quotient]
   ["[1][0]" refinement]
   ["[1][0]" resource]
   ["[1][0]" unit]
   ["[1][0]" variance]])

(template [<name>]
  [(documentation: <name>
     "The number of parameters, and the body, of a quantified type.")]

  [/.flat_univ_q]
  [/.flat_ex_q]
  )

(documentation: /.flat_function
  "The input, and the output of a function type."
  [(flat_function type)])

(documentation: /.flat_application
  "The quantified type, and its parameters, for a type-application."
  [(flat_application type)])

(template [<name>]
  [(documentation: <name>
     "The members of a composite type.")]

  [/.flat_variant]
  [/.flat_tuple]
  )

(documentation: /.format
  "A (readable) textual representable of a type."
  [(format type)])

(documentation: /.applied
  "To the extend possible, applies a quantified type to the given parameters."
  [(applied params func)])

(documentation: /.code
  (%.format "A representation of a type as code."
            \n "The code is such that evaluating it would yield the type value.")
  [(code type)])

(documentation: /.de_aliased
  "A (potentially named) type that does not have its name shadowed by other names."
  [(de_aliased type)])

(documentation: /.anonymous
  "A type without any names covering it."
  [(anonymous type)])

(template [<name>]
  [(documentation: <name>
     "A composite type, constituted by the given member types.")]

  [/.variant]
  [/.tuple]
  )

(documentation: /.function
  "A function type, with the given inputs and output."
  [(function inputs output)])

(documentation: /.application
  "An un-evaluated type application, with the given quantified type, and parameters."
  [(application params quant)])

(template [<name>]
  [(documentation: <name>
     "A quantified type, with the given number of parameters, and body.")]

  [/.univ_q]
  [/.ex_q]
  )

(documentation: /.quantified?
  "Only yields #1 for universally or existentially quantified types."
  [(quantified? type)])

(documentation: /.array
  "An array type, with the given level of nesting/depth, and the given element type."
  [(array depth element_type)])

(documentation: /.flat_array
  "The level of nesting/depth and element type for an array type."
  [(flat_array type)])

(documentation: /.array?
  "Is a type an array type?")

(documentation: /.:log!
  "Logs to the console/terminal the type of an expression."
  [(:log! (: Foo (foo expression)))
   "=>"
   "Expression: (foo expression)"
   "      Type: Foo"
   (foo expression)])

(documentation: /.:as
  (%.format "Casts a value to a specific type."
            \n "The specified type can depend on type variables of the original type of the value."
            \n "NOTE: Careless use of type-casts is an easy way to introduce bugs. USE WITH CAUTION.")
  [(: (Bar Bit Nat Text)
      (:as [a b c]
           (Foo a [b c])
           (Bar a b c)
           (: (Foo Bit [Nat Text])
              (foo expression))))])

(documentation: /.:sharing
  "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)))])

(documentation: /.:by_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))])

(.def: .public documentation
  (.List $.Module)
  ($.module /._
            "Basic functionality for working with types."
            [..flat_univ_q
             ..flat_ex_q
             ..flat_function
             ..flat_application
             ..flat_variant
             ..flat_tuple
             ..format
             ..applied
             ..code
             ..de_aliased
             ..anonymous
             ..variant
             ..tuple
             ..function
             ..application
             ..univ_q
             ..ex_q
             ..quantified?
             ..array
             ..flat_array
             ..array?
             ..:log!
             ..:as
             ..:sharing
             ..:by_example
             ($.default /.equivalence)]
            [/abstract.documentation
             /check.documentation
             /dynamic.documentation
             /implicit.documentation
             /poly.documentation
             /quotient.documentation
             /refinement.documentation
             /resource.documentation
             /unit.documentation
             /variance.documentation]))