Function definitions and variable annotations

changelog.md

@@ -0,0 +1,21 @@
+# 0.3.0 - WIP
+- `String` literals
+- Exponentiation operation on floats (and their `Descriptor` analysis)
+- Scientific notation accepted for floating-point literals
+- `None` type (and its constructor `None`) built-in.
+- `sqrt` function that is well-typed.
+- Gradable booleans and conditional expressions
+- `Species` and `Basis` descriptors 
+- Python-style `def` function blocks with typed arguments and `return`
+
+# 0.2.0 - PROPL 2026 announcement (June 15, 2026)
+- Pythonic syntax in types
+- Typing now includes implicit types with type dependency (for resolving Float which has kind `{d : Descriptor} -> d -> Type`
+- REPL `fortli`
+
+# 0.1.0 - Initial version
+
+- Straight line numerical code (with lambdas), Pythonic style.
+- Type checking (with annotations).
+Floats are graded abelian groups, graded by Descriptors which are generated by the free-abelian group over constructors names (which do not need defining and can be arbitrarily introduced, but must be guarded by Unit and Quantity constructors). 
+- Combinator for composing `Descriptor` values: `& : Descriptor -> Descriptor -> Descriptor` which behaves a bit like linear logic 'with' (additive conjunction).

examples/coriolis.frtl.output

@@ -0,0 +1 @@
+None

examples/diffusion.frtl.output

@@ -0,0 +1 @@
+None

examples/flow-rate.frtl

@@ -1,16 +1,23 @@
 ## Small-orifice flow problem (Torricelli's law)
+def small_orifice_flow(area, h):
+  """Area of the orifice"""
+  area : Float[Unit[m^2]]
 
-# Area of the orifice
-area : Float[Unit[m^2]] = 0.0
+  """Distance from water surface to orifice"""
+  h : Float[Unit[m]]
 
-# Acceleration of gravity
-gravity : Float[Unit[m / s^2]] = 9.8065
+  """Acceleration of gravity"""
+  gravity : Float[Unit[m / s^2]] = 9.8065
 
-#  Distance from water surface to orifice
-h : Float[Unit[m]] = 0.0
+  """Ratio of actual flow to ideal flow"""
+  discharge_coefficient : Float[Unit[1]] = 0.61
 
-# Ratio of actual flow to ideal flow
-discharge_coefficient : Float[Unit[1]] = 0.61
+  q : Float[Unit[m ^ 3 / s]] = (discharge_coefficient
+    * area * sqrt((2.0 : Float[Unit[1]]) * gravity * h))
 
-q : Float[Unit[m ^ 3 / s]] = (discharge_coefficient
-                               * area * sqrt((2.0 : Float[Unit[1]]) * gravity * h))
+  return q
+
+# Example
+area : Float[Unit[m^2]] = 10.0
+h    : Float[Unit[m]]   = 5.0
+it = small_orifice_flow(area, h)

examples/flow-rate.frtl.output

@@ -0,0 +1 @@
+60.406948

src/Lang/Desugar.hs

@@ -3,20 +3,29 @@
 
 module Lang.Desugar where
 
+-- Lowers a program into a desugared state (for simpler interpreter)
+
 import Lang.Syntax
+import Lang.TypeError
 
 import Control.Monad.Trans.State
-import Control.Monad.Trans.Writer
 import Control.Monad.Trans.Class     (lift)
 
 import Data.Foldable                 (traverse_)
+import qualified Data.Map.Lazy as Map
 
-newtype ST = ST { next_var :: Integer }
+-- Desugarer state
+data ST = ST
+    { next_var :: Integer
+    , pendingAnnotations :: Map.Map Identifier (Type 0)
+    , outputDefs :: [Def 'Desugared]
+    }
 
 initState :: ST
-initState = ST 0
+initState = ST 0 Map.empty []
 
-type Desugar = StateT ST (Writer [Def 'Desugared])
+-- Desugarer monad
+type Desugar = StateT ST (Either TypeError)
 
 freshVar :: Desugar Identifier
 freshVar = do
@@ -25,22 +34,113 @@ freshVar = do
     put $ st { next_var = i + 1 }
     return $ "_" ++ show i
 
-desugar :: Program 'Parsed -> Program 'Desugared
-desugar p = 
-    let m = traverse_ desugarDef p
-        (_, out) = runWriter (runStateT m initState)
-    in out
+-- Convert from a parsed program to a desugared one
+desugar :: Program 'Parsed -> Either TypeError (Program 'Desugared)
+desugar p = outputDefs <$> execStateT (traverse_ desugarDef p) initState
 
 -- | Add desugared definitions to the output of the desugaring pass.
 emitDefs :: [Def 'Desugared] -> Desugar ()
-emitDefs = lift . tell
+emitDefs defs = modify $ \st -> st { outputDefs = outputDefs st ++ defs }
 
 desugarDef :: Def 'Parsed -> Desugar ()
 desugarDef (TypeDef id ty1 ty2) = emitDefs [TypeDef id ty1 ty2]
 desugarDef (DataDef id cs ty)   = emitDefs [DataDef id cs ty]
 desugarDef (ImportDef spec)     = emitDefs [ImportDef spec]
 desugarDef (Return e)           = emitDefs [Return e]
-desugarDef (ValDef lhs e)       = do desugarVal lhs e
+desugarDef (AnnDef id ty) = do
+  -- Add the typing annotation of id
+  modify $ \st -> st { pendingAnnotations = Map.insert id ty (pendingAnnotations st) }
+desugarDef (FunDef id args body) = do
+  annotations <- pendingAnnotations <$> get
+  bodyExpr <- desugarBody annotations body
+  -- Get the types of arguments
+  typedArgs <- lift $ resolveFunctionParameterTypes args body
+  -- Build the function input type
+  let argType = functionArgType typedArgs
+  -- Rewrite the body expression to have the right type annotations
+  argVar <- freshVar
+  let bindArgs = bindFunctionArgs typedArgs (Var argVar) bodyExpr
+  -- Build the lambda
+  let functionExpr = Abs argVar (Just argType) bindArgs
+  emitDefs [ValDef (VarLhs id Nothing) functionExpr]
+
+desugarDef (ValDef lhs e) = do
+    lhs' <- applyPendingAnnotation lhs
+    desugarVal lhs' e
+
+-- | Resolve the declared types of a function's parameters before lowering its
+-- body to a lambda expression. Parameters can carry an optional legacy header
+-- annotation, while standalone annotations in the body support Python-style
+-- declarations such as @def f(x): x : T@. A body annotation takes precedence,
+-- keeping the parameter name next to its documentation and unit information.
+-- Every parameter must resolve to a type because the generated lambda is
+-- explicitly typed.
+resolveFunctionParameterTypes :: [(Identifier, Maybe (Type 0))] -> [Def 'Parsed] -> Either TypeError [(Identifier, Type 0)]
+resolveFunctionParameterTypes args body = traverse argumentType args
+    where
+        argumentType (arg, headerType) =
+            case [ty | AnnDef name ty <- body, name == arg] of
+                ty:_ | Just _ <- headerType ->
+                    Left $ WellFormednessError $ DuplicateParameterAnnotation arg
+                ty:_ -> Right (arg, ty)
+                [] -> case headerType of
+                    Just ty -> Right (arg, ty)
+                    Nothing -> Left $ WellFormednessError $ MissingParameterAnnotation arg
+
+-- From a list of identifiers and types, create a product type
+functionArgType :: [(Identifier, Type 0)] -> Type 0
+functionArgType [] = tyCon0 "()"
+functionArgType args = foldr1 ProdTy (map snd args)
+
+desugarBody :: Map.Map Identifier (Type 0) -> [Def 'Parsed] -> Desugar Expr
+desugarBody _ [] = return (Con "None" [])
+desugarBody _ (Return e : _) = return e
+desugarBody annotations (AnnDef id ty : defs) =
+    desugarBody (Map.insert id ty annotations) defs
+desugarBody annotations (ValDef lhs e : defs) = do
+    let (lhs', annotations') = applyAnnotation annotations lhs
+    rest <- desugarBody annotations' defs
+    bindLhs lhs' e rest
+desugarBody annotations (_ : defs) = desugarBody annotations defs
+
+applyPendingAnnotation :: Lhs 'Parsed -> Desugar (Lhs 'Parsed)
+applyPendingAnnotation lhs = do
+    st <- get
+    let (lhs', annotations) = applyAnnotation (pendingAnnotations st) lhs
+    put $ st { pendingAnnotations = annotations }
+    return lhs'
+
+-- | Apply and consume a preceding standalone annotation when the binding has
+-- no inline annotation. Inline annotations remain authoritative.
+applyAnnotation :: Map.Map Identifier (Type 0) -> Lhs 'Parsed -> (Lhs 'Parsed, Map.Map Identifier (Type 0))
+applyAnnotation annotations lhs@(VarLhs id Nothing) =
+    case Map.lookup id annotations of
+        Just ty -> (VarLhs id (Just ty), Map.delete id annotations)
+        Nothing -> (lhs, annotations)
+applyAnnotation annotations lhs = (lhs, annotations)
+
+bindLhs :: Lhs 'Parsed -> Expr -> Expr -> Desugar Expr
+bindLhs (VarLhs x (Just ty)) e rest = return (Let x (Sig e ty) rest)
+bindLhs (VarLhs x Nothing) e rest = return (Let x e rest)
+bindLhs (PairLhs l1 l2) e rest = do
+    tmp <- freshVar
+    rest' <- bindLhs l1 (Fst (Var tmp)) rest
+    bindLhs l2 (Snd (Var tmp)) (Let tmp e rest')
+
+bindFunctionArgs :: [(Identifier, Type 0)] -> Expr -> Expr -> Expr
+bindFunctionArgs [] _ body = body
+bindFunctionArgs [(x, _)] arg body = Let x arg body
+bindFunctionArgs args arg body =
+    foldr bind body (zip args (pairProjections (length args) arg))
+  where
+    bind ((x, _), projection) rest = Let x projection rest
+
+pairProjections :: Int -> Expr -> [Expr]
+pairProjections count arg =
+    [ projection index | index <- [0 .. count - 1] ]
+  where
+    projection 0 = Fst arg
+    projection index = Snd (iterate Snd arg !! (index - 1))
 
 -- (a, (b1, b2)) = c
 -- _0 = c

src/Lang/Frontend.hs

@@ -50,21 +50,27 @@ run report fname = do
       input <- readFile fname
       case parseProgram fname input of
         Right (parsetree, options) -> do
-          let ast = desugar parsetree
-          -- Evaluate
-          let (env, normalForm) = interpret options ast
-          -- Typing
-          case typeInference options ast of
-              Left err -> do
-                let ?srcFile = fname
-                putStrLn $ ansi_bold <> ansi_red
-                        <> "Not well-typed.\n" <> errorToString err <> ansi_reset
-                return $ Left (errorToString err)
-              Right (ctxt, ty) -> do
-                putStrLn $ ansi_bold <> ansi_green
-                        <> "Well-typed " <> ansi_reset
-                        <> ansi_bold <> "as " <> ansi_reset <> pprint ty
-                return $ Right (parsetree, options, env, normalForm, ctxt)
+          case desugar parsetree of
+            Left err -> do
+              let ?srcFile = fname
+              putStrLn $ ansi_bold <> ansi_red
+                      <> "Not well-formed.\n" <> errorToString err <> ansi_reset
+              return $ Left (errorToString err)
+            Right ast -> do
+              -- Evaluate
+              let (env, normalForm) = interpret options ast
+              -- Typing
+              case typeInference options ast of
+                Left err -> do
+                  let ?srcFile = fname
+                  putStrLn $ ansi_bold <> ansi_red
+                    <> "Not well-typed.\n" <> errorToString err <> ansi_reset
+                  return $ Left (errorToString err)
+                Right (ctxt, ty) -> do
+                  putStrLn $ ansi_bold <> ansi_green
+                    <> "Well-typed " <> ansi_reset
+                    <> ansi_bold <> "as " <> ansi_reset <> pprint ty
+                  return $ Right (parsetree, options, env, normalForm, ctxt)
         Left msg -> do
           putStrLn $ ansi_red ++ "Error: " ++ ansi_reset ++ msg
           return $ Left msg

src/Lang/Lexer.x

@@ -20,6 +20,7 @@ $alpha  = [a-zA-Z\_\-]
 $lower  = [a-z]
 $upper  = [A-Z]
 $eol    = [\n]
+$hwhite = [\ \t]
 $alphanum  = [$alpha $digit \_]
 @sym    = ($lower | $upper) ($alphanum | \')*
 @tyvar    = \' @sym
@@ -32,15 +33,16 @@ $alphanum  = [$alpha $digit \_]
 
 tokens :-
 
-  $white*$eol                   { \p s -> TokenNL p }
+  $hwhite*$eol                  { \p s -> TokenNL p }
   $eol+                         { \p s -> TokenNL p }
-  $white+                       ;
+  $hwhite+                      ;
   "#" .*                        ;
   @tyvar                          { \p s -> TokenTyVar p (tail s) }
   lang\.@langPrag               { \p s -> TokenLang p s }
   forall                        { \p _ -> TokenForall p }
   data                          { \p s -> TokenData p }
   let                           { \p s -> TokenLet p }
+  def                           { \p s -> TokenDef p }
   in                            { \p s -> TokenIn p }
   succ                          { \p s -> TokenSucc p }
   zero                          { \p s -> TokenZero p }
@@ -95,6 +97,7 @@ tokens :-
 data Token
   = TokenLang     AlexPosn String
   | TokenData     AlexPosn
+  | TokenDef      AlexPosn
   | TokenCase     AlexPosn
   | TokenNatCase  AlexPosn
   | TokenOf       AlexPosn
@@ -115,6 +118,8 @@ data Token
   | TokenLParen   AlexPosn
   | TokenRParen   AlexPosn
   | TokenNL       AlexPosn
+  | TokenIndent   AlexPosn
+  | TokenDedent   AlexPosn
   | TokenSig      AlexPosn
   | TokenEquiv    AlexPosn
   | TokenHole     AlexPosn
@@ -161,7 +166,78 @@ tyVarString :: Token -> String
 tyVarString (TokenTyVar _ x) = x
 tyVarString t = error $ "Not a type variable " ++ show t
 
-scanTokens = alexScanTokens . stripDocstrings >>= (return . trim)
+scanTokens = alexScanTokens . stripDocstrings >>= (return . trim . layout)
+
+-- Add layout markers for function bodies. Existing multiline expressions use
+-- indentation for readability, so layout is activated only after a def header.
+layout :: [Token] -> [Token]
+layout tokens = go tokens [] False 0
+  where
+    go [] _ True _ = [TokenDedent (AlexPn 0 0 0)]
+    go [] _ False _ = []
+    go (t:ts) stack active parenDepth =
+      case t of
+        TokenNL p ->
+          let (next, _) = nextNonNL ts
+              lineHeader = isDefHeader currentLine
+              nextColumn = maybe 0 (snd . getPos) next
+              (markers, stack', active')
+                | not active && lineHeader && nextColumn > lineColumn currentLine =
+                    ([TokenIndent p], [nextColumn], True)
+                | active && nextColumn < head stack =
+                    ([TokenDedent p], [], False)
+                | otherwise = ([], stack, active)
+              newline = if (active && parenDepth == 0)
+                           || lineHeader || lineStartsImport currentLine
+                        then [t]
+                        else []
+          in newline ++ markers ++ goWithLine [] ts stack' active' parenDepth
+        _ -> t : goWithLine (currentLine ++ [t]) ts stack active (parenDepth + parenthesisDepth t)
+      where
+        currentLine = []
+
+    goWithLine _ [] _ True _ = [TokenDedent (AlexPn 0 0 0)]
+    goWithLine line (t:ts) stack active parenDepth =
+      case t of
+        TokenNL p ->
+          let (next, _) = nextNonNL ts
+              lineHeader = isDefHeader line
+              nextColumn = maybe 0 (snd . getPos) next
+              (markers, stack', active')
+                | not active && lineHeader && nextColumn > lineColumn line =
+                    ([TokenIndent p], [nextColumn], True)
+                | active && nextColumn < head stack =
+                    ([TokenDedent p], [], False)
+                | otherwise = ([], stack, active)
+              newline = if (active && parenDepth == 0)
+                           || lineHeader || lineStartsImport line
+                        then [t]
+                        else []
+          in newline ++ markers ++ goWithLine [] ts stack' active' parenDepth
+        _ -> t : goWithLine (line ++ [t]) ts stack active (parenDepth + parenthesisDepth t)
+    goWithLine _ [] _ False _ = []
+
+    nextNonNL [] = (Nothing, [])
+    nextNonNL (TokenNL _ : ts) = nextNonNL ts
+    nextNonNL (t:ts) = (Just t, ts)
+
+    lineColumn [] = 0
+    lineColumn (t:_) = snd (getPos t)
+
+    isDefHeader line = any isDef line && any isColon line
+    isDef (TokenDef _) = True
+    isDef _ = False
+    isColon (TokenSig _) = True
+    isColon _ = False
+
+    parenthesisDepth (TokenLParen _) = 1
+    parenthesisDepth (TokenRParen _) = -1
+    parenthesisDepth _ = 0
+
+    lineStartsImport (TokenLang _ _ : _) = True
+    lineStartsImport (TokenImport _ : _) = True
+    lineStartsImport (TokenFrom _ : _) = True
+    lineStartsImport _ = False
 
 -- Strip Python-style triple-quoted docstrings before lexing.
 -- We preserve newlines to keep parser layout/error positions stable.