User-facing API suggestion

1 files changed, 58 insertions, 4 deletions

diff --git a/src/CHAD/Language/AST.hs b/src/CHAD/Language/AST.hs
index b270844..502a2b3 100644
--- a/src/CHAD/Language/AST.hs
+++ b/src/CHAD/Language/AST.hs
@@ -28,6 +28,8 @@ import CHAD.Data
 import CHAD.Drev.Types
 
 
+-- | A named expression: variables have names, not De Bruijn indices.
+-- Otherwise essentially identical to 'Expr'.
 type NExpr :: [(Symbol, Ty)] -> Ty -> Type
 data NExpr env t where
   -- lambda calculus
@@ -99,7 +101,14 @@ data NExpr env t where
   NEUnnamed :: Ex unenv t -> SList (NExpr env) unenv -> NExpr env t
 deriving instance Show (NExpr env t)
 
+-- | Look up the type of a name in a named environment.
 type Lookup name env = Lookup1 (name == "_") name env
+-- | This curious stack of type families is used instead of normal pattern
+-- matching so the decidable boolean predicate "==" is used. This means that
+-- introducing evidence of @(name1 == name2) ~ False@ may allow a certain
+-- lookup to reduce even if the names in question are not statically known.
+-- This flexibility is used with e.g. 'assertSymbolDistinct' in
+-- 'CHAD.Language.fold1i'.
 type family Lookup1 eqblank name env where
   Lookup1 True _ _ = TypeError (Text "Attempt to use variable with name '_'")
   Lookup1 False name env = Lookup2 name env
@@ -160,10 +169,20 @@ data NEnv env where
   NTop :: NEnv '[]
   NPush :: NEnv env -> Var name t -> NEnv ('(name, t) : env)
 
--- | First (outermost) parameter on the outside, on the left.
--- * env: environment of this function (grows as you go deeper inside lambdas)
--- * env': environment of the body of the function
--- * params: parameters of the function (difference between env and env'), first (outermost) argument at the head of the list
+-- | A named /function/. These can be used in only two ways: they can be
+-- converted to an unnamed 'Expr' using 'fromNamed', and they can be inlined
+-- using 'CHAD.Language.inline'.
+--
+-- * @env@: environment of this function (smaller than @env'@; grows as you descend under lambdas)
+-- * @env'@: environment of the body of the function
+--
+-- For example, a function @(\\(x :: a) (y :: b) -> _ :: c)@ with two free
+-- variables, @u :: t1@ and @v :: t2@, would be represented with a value of the
+-- following type:
+--
+-- @
+-- NFun '['("v", t2), '("u", t1)] '['("y", b), '("x", a), '("v", t2), '("u", t1)] c
+-- @
 data NFun env env' t where
   NLam :: Var name a -> NFun ('(name, a) : env) env' t -> NFun env env' t
   NBody :: NExpr env' t -> NFun env' env' t
@@ -179,6 +198,41 @@ envFromNEnv (NPush env (Var _ t)) = t `SCons` envFromNEnv env
 inlineNFun :: NFun '[] envB t -> SList (NExpr env) (UnName envB) -> NExpr env t
 inlineNFun fun args = NEUnnamed (fromNamed fun) args
 
+-- | Convert a named function to an unnamed expression with free variables,
+-- ready for consumption by the rest of this library. The function must be
+-- closed (meaning that the function as a whole cannot have free variables),
+-- and the arguments of the function are realised as free variables of the
+-- resulting expression. Typical usage looks as follows:
+--
+-- @
+-- {-# LANGUAGE OverloadedLabels #-}
+-- import CHAD.Language
+-- 'fromNamed' $ 'CHAD.Language.lambda' \@(TScal TF64) #x $ 'CHAD.Language.lambda' \@(TScal TI64) #i $ 'CHAD.Language.body' $ #x + 'CHAD.Language.toFloat_' #i
+--   :: 'Ex' '[TScal TI64, TScal TF64] (TScal TF64)
+-- @
+--
+-- The rest of the library generally considers expressions with free variables
+-- to stand in for "functions", by considering the free variables as the
+-- function's inputs.
+--
+-- Note that while environments normally grow to the right (e.g. in type theory
+-- notation), as they as type-level lists here, they grow to the /left/. This
+-- is why the second (innermost) argument of the example, @i@, ends up at the
+-- head of the environment of the constructed expression.
+--
+-- __Type applications__: The type applications to 'CHAD.Language.lambda' above
+-- are good practice, but not always necessary; if GHC can infer the type of
+-- the argument from the body of the expression, the type application is
+-- unnecessary.
+--
+-- __Variables__: The major element of syntactic sugar in this module is using
+-- OverloadedLabels for variable names. Variables are represented in 'NExpr'
+-- (and thus 'NFun') using the 'Var' type; you should never have to manually
+-- construct a 'Var'. Instead, 'Var' implements 'IsLabel' and as such can be
+-- produced with the syntax @#name@, where "name" is the name of the variable.
+-- This syntax produces a polymorphic variable reference whose (embedded) type
+-- is left to GHC's type inference engine using a 'KnownTy' constraint. See
+-- also 'CHAD.Language.let_'.
 fromNamed :: NFun '[] env t -> Ex (UnName env) t
 fromNamed = fromNamedFun NTop