lux/type/check

Type-checking functionality.

Very useful for writing advanced macros.

Types

Check

(type: (Check a)
  (-> Context (lux/data/error;Error [Context a])))

Context

(type: Context
  {#var-counter Id
   #ex-counter Id
   #bindings (lux/data/struct/dict;Dict Id (lux;Maybe lux;Type))
   #fixpoints Fixpoints})

Fixpoints

(type: Fixpoints
  (lux;List [[lux;Type lux;Type] lux;Bool]))

Id

(type: Id
  lux;Nat)

Structs

Applicative<Check>

(lux/control/applicative;Applicative Check)

Functor<Check>

(lux/control/functor;Functor Check)

Monad<Check>

(lux/control/monad;Monad Check)

Values

(check expected actual)

Type-check to ensure that the 'expected' type subsumes the 'actual' type.

(-> lux;Type lux;Type (Check lux;Unit))

(checks? expected actual)

A simple type-checking function that just returns a yes/no answer.

(-> lux;Type lux;Type lux;Bool)

(clear-var id)

(-> Id (Check lux;Unit))

create-var

(Check [Id lux;Type])

(delete-var id)

(-> Id (Check lux;Unit))

existential

A producer of existential types.

(Check [Id lux;Type])

(fail message)

(All [a] (-> lux;Text (Check a)))

fresh-context

Context

get-context

(Check Context)

(read-var id)

(-> Id (Check lux;Type))

(run context proc)

(All [a] (-> Context (Check a) (lux/data/error;Error a)))

(with-var k)

(All [a] (-> (-> [Id lux;Type] (Check a)) (Check a)))

(write-var id type)

(-> Id lux;Type (Check lux;Unit))