From e549c2e92916d69f28da9a52653e07939f93742c Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 16:59:29 +0100 Subject: [PATCH 1/9] definitions and indentation --- examples/flow-rate.frtl | 23 +++++------ src/Lang/Desugar.hs | 41 ++++++++++++++++++++ src/Lang/Lexer.x | 82 ++++++++++++++++++++++++++++++++++++++-- src/Lang/Parser.y | 26 +++++++++++-- src/Lang/PrettyPrint.hs | 2 +- src/Lang/Semantics.hs | 2 +- src/Lang/Substitution.hs | 4 +- src/Lang/Syntax.hs | 19 +++++----- src/Lang/Types.hs | 8 +++- 9 files changed, 175 insertions(+), 32 deletions(-) diff --git a/examples/flow-rate.frtl b/examples/flow-rate.frtl index 3828cc6..e2b67b4 100644 --- a/examples/flow-rate.frtl +++ b/examples/flow-rate.frtl @@ -1,16 +1,17 @@ ## Small-orifice flow problem (Torricelli's law) +def small_orifice_flow(area : Float[Unit[m^2]], h : Float[Unit[m]]): + """ + area : Area of the orifice + h : Distance from water surface to orifice + """ -# Area of the orifice -area : Float[Unit[m^2]] = 0.0 + # Acceleration of gravity + gravity : Float[Unit[m / s^2]] = 9.8065 -# Acceleration of gravity -gravity : Float[Unit[m / s^2]] = 9.8065 + # Ratio of actual flow to ideal flow + discharge_coefficient : Float[Unit[1]] = 0.61 -# Distance from water surface to orifice -h : Float[Unit[m]] = 0.0 + q : Float[Unit[m ^ 3 / s]] = (discharge_coefficient + * area * sqrt((2.0 : Float[Unit[1]]) * gravity * h)) -# 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)) \ No newline at end of file + return q \ No newline at end of file diff --git a/src/Lang/Desugar.hs b/src/Lang/Desugar.hs index afc4920..dd406ab 100644 --- a/src/Lang/Desugar.hs +++ b/src/Lang/Desugar.hs @@ -40,8 +40,49 @@ 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 (FunDef id args body) = do + bodyExpr <- desugarBody body + let argType = functionArgType args + bindArgs = bindFunctionArgs args (Var "_args") bodyExpr + functionExpr = Abs "_args" (Just argType) bindArgs + emitDefs [ValDef (VarLhs id Nothing) functionExpr] desugarDef (ValDef lhs e) = do desugarVal lhs e +functionArgType :: [(Identifier, Type 0)] -> Type 0 +functionArgType [( _, ty)] = ty +functionArgType args = foldr1 ProdTy (map snd args) + +desugarBody :: [Def 'Parsed] -> Desugar Expr +desugarBody [] = return (Con "None" []) +desugarBody (Return e : _) = return e +desugarBody (ValDef lhs e : defs) = do + rest <- desugarBody defs + bindLhs lhs e rest +desugarBody (_ : defs) = desugarBody defs + +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 -- a = fst _0 diff --git a/src/Lang/Lexer.x b/src/Lang/Lexer.x index 12440bd..5f0b658 100755 --- a/src/Lang/Lexer.x +++ b/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. diff --git a/src/Lang/Parser.y b/src/Lang/Parser.y index 7d51c5d..21b6de2 100644 --- a/src/Lang/Parser.y +++ b/src/Lang/Parser.y @@ -25,6 +25,9 @@ import Lang.Options %token nl { TokenNL _ } data { TokenData _ } + def { TokenDef _ } + indent { TokenIndent _ } + dedent { TokenDedent _ } from { TokenFrom _ } import { TokenImport _ } cast { TokenCast _ } @@ -115,6 +118,7 @@ ImportList :: { [Identifier] } Defs :: { [Option] -> Program 'Parsed } : Def NL Defs { \opts -> ($1 opts) : ($3 opts) } + | Def Defs { \opts -> ($1 opts) : ($2 opts) } | return Expr { \opts -> [Return ($2 opts)] } | Def { \opts -> [$1 opts] } @@ -124,8 +128,23 @@ NL :: { () } Def :: { [Option] -> Def 'Parsed} : Lhs '=' Expr { \opts -> ValDef ($1 opts) ($3 opts) } + | def IDENT '(' Parameters ')' ':' nl indent BlockDefs dedent + { \opts -> FunDef (symString $2) ($4 opts) ($9 opts) } | data IDENT ':' Kind '=' ConstructorList { \opts -> DataDef (symString $2) ($6 opts) ($4 opts) } +Parameters :: { [Option] -> [(Identifier, Type 0)] } + : IDENT ':' Type ',' Parameters + { \opts -> (symString $1, $3 opts) : ($5 opts) } + | IDENT ':' Type { \opts -> [(symString $1, $3 opts)] } + | {- empty -} { \_ -> [] } + +BlockDefs :: { [Option] -> [Def 'Parsed] } + : nl BlockDefs { $2 } + | Def nl BlockDefs { \opts -> ($1 opts) : ($3 opts) } + | return Expr nl { \opts -> [Return ($2 opts)] } + | Def { \opts -> [$1 opts] } + | return Expr { \opts -> [Return ($2 opts)] } + Lhs :: { [Option] -> Lhs 'Parsed } : IDENT { \opts -> VarLhs (symString $1) Nothing } | IDENT ':' Type { \opts -> VarLhs (symString $1) (Just $ $3 opts) } @@ -140,10 +159,9 @@ ConstructorList Expr :: { [Option] -> Expr } : let IDENT '=' Expr in Expr - { \opts -> - MkGenLet (mkPos $1) (symString $2) ($4 opts) ($6 opts) } + { \opts -> MkLet (mkPos $1) (symString $2) ($4 opts) ($6 opts) } - -- TODO: probably needs reconciling with lambda syntax + -- TODO: probably needs reconciling with lambda syntax | Lam IDENT '->' Expr { \opts -> MkTyAbs (mkPos $1) (symString $2) ($4 opts) } @@ -200,7 +218,7 @@ Kind : Kind '->' Kind { \opts -> FunTy ($1 opts) ($3 opts) } | IDENT { \opts -> case symString $1 of k -> tyCon1 k } - + Type :: { [Option] -> Type 0 } Type : Type '->' Type { \opts -> FunTy ($1 opts) ($3 opts) } diff --git a/src/Lang/PrettyPrint.hs b/src/Lang/PrettyPrint.hs index 7b88ac8..02c407b 100644 --- a/src/Lang/PrettyPrint.hs +++ b/src/Lang/PrettyPrint.hs @@ -39,7 +39,7 @@ instance PrettyPrint Expr where pprint (TyAbs var e) = "/\\" ++ var ++ " -> " ++ pprint e pprint (TyEmbed t) = "@" ++ bracket_pprint t -- ML - pprint (GenLet x e1 e2) = "let " ++ x ++ " = " ++ pprint e1 ++ " in " ++ pprint e2 + pprint (Let x e1 e2) = "let " ++ x ++ " = " ++ pprint e1 ++ " in " ++ pprint e2 -- PCF expressions pprint Zero = "zero" pprint Succ = "succ" diff --git a/src/Lang/Semantics.hs b/src/Lang/Semantics.hs index 4b6c6ff..030bf36 100644 --- a/src/Lang/Semantics.hs +++ b/src/Lang/Semantics.hs @@ -68,7 +68,7 @@ bigStep env opts (Var x) = case lookup x env of case lookup x dataConstructors of Just _ -> Right (Con x []) Nothing -> Left $ "Unbound variable: " ++ x -bigStep env opts (GenLet x e1 e2) = do +bigStep env opts (Let x e1 e2) = do v1 <- bigStep env opts e1 bigStep ((x, v1) : env) opts e2 diff --git a/src/Lang/Substitution.hs b/src/Lang/Substitution.hs index c575b1c..69c6789 100644 --- a/src/Lang/Substitution.hs +++ b/src/Lang/Substitution.hs @@ -31,8 +31,8 @@ substituteExpr (Sig e t) s = Sig (substituteExpr e s) t -- ML -substituteExpr (GenLet x e1 e2) s = - let (x' , e2') = substitute_binding x e2 s in GenLet x' (substituteExpr e1 s) e2' +substituteExpr (Let x e1 e2) s = + let (x' , e2') = substitute_binding x e2 s in Let x' (substituteExpr e1 s) e2' -- Casts substituteExpr (Cast e) s = diff --git a/src/Lang/Syntax.hs b/src/Lang/Syntax.hs index 50346e0..f8c9e22 100644 --- a/src/Lang/Syntax.hs +++ b/src/Lang/Syntax.hs @@ -32,6 +32,7 @@ type Program (p :: Phase) = [Def p] data Def (p :: Phase) where ValDef :: Lhs p -> Expr -> Def p + FunDef :: Identifier -> [(Identifier, Type 0)] -> [Def p] -> Def p TypeDef :: Identifier -> Type n -> Type (1 + n) -> Def p DataDef :: Identifier -> [(Identifier, [Type n])] -> Type (1 + n) -> Def p -- Currently not implemented beyond front end ImportDef :: ImportSpec -> Def p @@ -59,7 +60,7 @@ data Expr where MkSig :: Maybe SrcPos -> Expr -> Type 0 -> Expr MkTyAbs :: Maybe SrcPos -> Identifier -> Expr -> Expr MkTyEmbed :: Maybe SrcPos -> Type 0 -> Expr - MkGenLet :: Maybe SrcPos -> Identifier -> Expr -> Expr -> Expr + MkLet :: Maybe SrcPos -> Identifier -> Expr -> Expr -> Expr MkCast :: Maybe SrcPos -> Expr -> Expr MkZero :: Maybe SrcPos -> Expr MkSucc :: Maybe SrcPos -> Expr @@ -89,7 +90,7 @@ exprPos (MkVar p _) = p exprPos (MkSig p _ _) = p exprPos (MkTyAbs p _ _) = p exprPos (MkTyEmbed p _) = p -exprPos (MkGenLet p _ _ _) = p +exprPos (MkLet p _ _ _) = p exprPos (MkCast p _) = p exprPos (MkZero p) = p exprPos (MkSucc p) = p @@ -137,9 +138,9 @@ pattern TyEmbed :: Type 0 -> Expr pattern TyEmbed t <- MkTyEmbed _ t where TyEmbed t = MkTyEmbed Nothing t -pattern GenLet :: Identifier -> Expr -> Expr -> Expr -pattern GenLet x e1 e2 <- MkGenLet _ x e1 e2 - where GenLet x e1 e2 = MkGenLet Nothing x e1 e2 +pattern Let :: Identifier -> Expr -> Expr -> Expr +pattern Let x e1 e2 <- MkLet _ x e1 e2 + where Let x e1 e2 = MkLet Nothing x e1 e2 pattern Cast :: Expr -> Expr pattern Cast e <- MkCast _ e @@ -217,11 +218,11 @@ pattern Cond :: Expr -> Expr -> Expr -> Expr pattern Cond e1 e2 e3 <- MkCond _ e1 e2 e3 where Cond e1 e2 e3 = MkCond Nothing e1 e2 e3 -{-# COMPLETE MkAbs, MkApp, MkVar, MkSig, MkTyAbs, MkTyEmbed, MkGenLet, MkCast, +{-# COMPLETE MkAbs, MkApp, MkVar, MkSig, MkTyAbs, MkTyEmbed, MkLet, MkCast, MkZero, MkSucc, MkNatCase, MkFix, MkPair, MkFst, MkSnd, MkInl, MkInr, MkCase, MkNumFloat, MkNumInteger, MkStringConst, MkBinOp, MkCon, MkCond #-} -{-# COMPLETE Abs, App, Var, Sig, TyAbs, TyEmbed, GenLet, Cast, +{-# COMPLETE Abs, App, Var, Sig, TyAbs, TyEmbed, Let, Cast, Zero, Succ, NatCase, Fix, Pair, Fst, Snd, Inl, Inr, Case, NumFloat, NumInteger, StringConst, BinOp, Con, Cond #-} @@ -333,7 +334,7 @@ instance Term Expr where boundVars (App e1 e2) = boundVars e1 `Set.union` boundVars e2 boundVars (Var var) = Set.empty boundVars (Sig e _) = boundVars e - boundVars (GenLet var e1 e2) = var `Set.insert` (boundVars e1 `Set.union` boundVars e2) + boundVars (Let var e1 e2) = var `Set.insert` (boundVars e1 `Set.union` boundVars e2) boundVars (Cast e) = boundVars e boundVars (NatCase e e1 (x,e2)) = x `Set.insert` (boundVars e `Set.union` boundVars e1 `Set.union` boundVars e2) @@ -356,7 +357,7 @@ instance Term Expr where freeVars (App e1 e2) = freeVars e1 `Set.union` freeVars e2 freeVars (Var var) = Set.singleton var freeVars (Sig e _) = freeVars e - freeVars (GenLet var e1 e2) = Set.delete var (freeVars e1 `Set.union` freeVars e2) + freeVars (Let var e1 e2) = Set.delete var (freeVars e1 `Set.union` freeVars e2) freeVars (Cast e) = freeVars e freeVars (NatCase e e1 (x,e2)) = freeVars e `Set.union` freeVars e1 `Set.union` (Set.delete x (freeVars e2)) diff --git a/src/Lang/Types.hs b/src/Lang/Types.hs index fcd4fbe..0d41a01 100644 --- a/src/Lang/Types.hs +++ b/src/Lang/Types.hs @@ -277,6 +277,10 @@ synth_ gamma (Var x) = Just ty -> Right ty Nothing -> Left $ VariableNotFound x +synth_ gamma (Let x e1 e2) = do + ty1 <- synth gamma e1 + synth ((x, ty1) : gamma) e2 + {- @@ -310,7 +314,9 @@ synth_ gamma (App (Abs x Nothing e1) (Sig e2 tyA)) = synth_ gamma (Abs x (Just tyA) e) = case checkKind tyA type0 of Left err -> Left err - Right tyA' -> synth ((x, tyA') : gamma) e + Right tyA' -> do + tyB <- synth ((x, tyA') : gamma) e + Right (FunTy tyA' tyB) -- Type checking a type speciaisation synth_ gamma (App e (TyEmbed tau')) = From 9e574d31b6b2927f1fd9aec6ee5b21499b8b14c2 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 17:41:32 +0100 Subject: [PATCH 2/9] annotations allowed on their own --- examples/flow-rate.frtl | 15 ++++++++------- src/Lang/Desugar.hs | 24 ++++++++++++++++++++++-- src/Lang/Parser.y | 9 ++++++--- src/Lang/Syntax.hs | 3 ++- src/Lang/Types.hs | 9 ++++++--- 5 files changed, 44 insertions(+), 16 deletions(-) diff --git a/examples/flow-rate.frtl b/examples/flow-rate.frtl index e2b67b4..a3d9ae3 100644 --- a/examples/flow-rate.frtl +++ b/examples/flow-rate.frtl @@ -1,14 +1,15 @@ ## Small-orifice flow problem (Torricelli's law) -def small_orifice_flow(area : Float[Unit[m^2]], h : Float[Unit[m]]): - """ - area : Area of the orifice - h : Distance from water surface to orifice - """ +def small_orifice_flow(area, h): + """Area of the orifice""" + area : Float[Unit[m^2]] - # Acceleration of gravity + """Distance from water surface to orifice""" + h : Float[Unit[m]] + + """Acceleration of gravity""" gravity : Float[Unit[m / s^2]] = 9.8065 - # Ratio of actual flow to ideal flow + """Ratio of actual flow to ideal flow""" discharge_coefficient : Float[Unit[1]] = 0.61 q : Float[Unit[m ^ 3 / s]] = (discharge_coefficient diff --git a/src/Lang/Desugar.hs b/src/Lang/Desugar.hs index dd406ab..7e0898f 100644 --- a/src/Lang/Desugar.hs +++ b/src/Lang/Desugar.hs @@ -40,14 +40,33 @@ 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 (AnnDef _ _) = return () desugarDef (FunDef id args body) = do bodyExpr <- desugarBody body - let argType = functionArgType args - bindArgs = bindFunctionArgs args (Var "_args") bodyExpr + let typedArgs = functionArguments args body + argType = functionArgType typedArgs + bindArgs = bindFunctionArgs typedArgs (Var "_args") bodyExpr functionExpr = Abs "_args" (Just argType) bindArgs emitDefs [ValDef (VarLhs id Nothing) functionExpr] desugarDef (ValDef lhs e) = do 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. +functionArguments :: [(Identifier, Maybe (Type 0))] -> [Def 'Parsed] -> [(Identifier, Type 0)] +functionArguments args body = map argumentType args + where + argumentType (arg, headerType) = + case [ty | AnnDef name ty <- body, name == arg] of + ty:_ -> (arg, ty) + [] -> case headerType of + Just ty -> (arg, ty) + Nothing -> error $ "Missing type annotation for function parameter " ++ arg + functionArgType :: [(Identifier, Type 0)] -> Type 0 functionArgType [( _, ty)] = ty functionArgType args = foldr1 ProdTy (map snd args) @@ -55,6 +74,7 @@ functionArgType args = foldr1 ProdTy (map snd args) desugarBody :: [Def 'Parsed] -> Desugar Expr desugarBody [] = return (Con "None" []) desugarBody (Return e : _) = return e +desugarBody (AnnDef _ _ : defs) = desugarBody defs desugarBody (ValDef lhs e : defs) = do rest <- desugarBody defs bindLhs lhs e rest diff --git a/src/Lang/Parser.y b/src/Lang/Parser.y index 21b6de2..2b97f07 100644 --- a/src/Lang/Parser.y +++ b/src/Lang/Parser.y @@ -128,14 +128,17 @@ NL :: { () } Def :: { [Option] -> Def 'Parsed} : Lhs '=' Expr { \opts -> ValDef ($1 opts) ($3 opts) } + | IDENT ':' Type { \opts -> AnnDef (symString $1) ($3 opts) } | def IDENT '(' Parameters ')' ':' nl indent BlockDefs dedent { \opts -> FunDef (symString $2) ($4 opts) ($9 opts) } | data IDENT ':' Kind '=' ConstructorList { \opts -> DataDef (symString $2) ($6 opts) ($4 opts) } -Parameters :: { [Option] -> [(Identifier, Type 0)] } +Parameters :: { [Option] -> [(Identifier, Maybe (Type 0))] } : IDENT ':' Type ',' Parameters - { \opts -> (symString $1, $3 opts) : ($5 opts) } - | IDENT ':' Type { \opts -> [(symString $1, $3 opts)] } + { \opts -> (symString $1, Just ($3 opts)) : ($5 opts) } + | IDENT ':' Type { \opts -> [(symString $1, Just ($3 opts))] } + | IDENT ',' Parameters { \opts -> (symString $1, Nothing) : ($3 opts) } + | IDENT { \_ -> [(symString $1, Nothing)] } | {- empty -} { \_ -> [] } BlockDefs :: { [Option] -> [Def 'Parsed] } diff --git a/src/Lang/Syntax.hs b/src/Lang/Syntax.hs index f8c9e22..d1c38b2 100644 --- a/src/Lang/Syntax.hs +++ b/src/Lang/Syntax.hs @@ -32,7 +32,8 @@ type Program (p :: Phase) = [Def p] data Def (p :: Phase) where ValDef :: Lhs p -> Expr -> Def p - FunDef :: Identifier -> [(Identifier, Type 0)] -> [Def p] -> Def p + AnnDef :: Identifier -> Type 0 -> Def p + FunDef :: Identifier -> [(Identifier, Maybe (Type 0))] -> [Def p] -> Def p TypeDef :: Identifier -> Type n -> Type (1 + n) -> Def p DataDef :: Identifier -> [(Identifier, [Type n])] -> Type (1 + n) -> Def p -- Currently not implemented beyond front end ImportDef :: ImportSpec -> Def p diff --git a/src/Lang/Types.hs b/src/Lang/Types.hs index 0d41a01..50bca02 100644 --- a/src/Lang/Types.hs +++ b/src/Lang/Types.hs @@ -100,9 +100,12 @@ check_ gamma (StringConst _) ty = _ -> Left $ TypeCheckFailure (integerTy unitDescription) ty "Expecting String type." check_ gamma (Sig e tyA) ty = - case typeEquality ty (IsSpec tyA) of - Right () -> check_ gamma e tyA - Left err -> Left $ TypeCheckFailure tyA ty (let ?srcFile = "" in errorToString err) + case checkKind tyA type0 of + Left err -> Left err + Right tyA' -> + case typeEquality ty (IsSpec tyA') of + Right () -> check_ gamma e tyA' + Left err -> Left $ TypeCheckFailure tyA' ty (let ?srcFile = "" in errorToString err) {-- From a82baeaaa58f4485aab0d9f4bcd1b045435c5690 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 20:43:27 +0100 Subject: [PATCH 3/9] expand example --- examples/flow-rate.frtl | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/examples/flow-rate.frtl b/examples/flow-rate.frtl index a3d9ae3..99eb0b9 100644 --- a/examples/flow-rate.frtl +++ b/examples/flow-rate.frtl @@ -15,4 +15,9 @@ def small_orifice_flow(area, h): q : Float[Unit[m ^ 3 / s]] = (discharge_coefficient * area * sqrt((2.0 : Float[Unit[1]]) * gravity * h)) - return q \ No newline at end of file + return q + +# Example +area : Float[Unit[m^2]] = 10.0 +h : Float[Unit[m]] = 5.0 +it = small_orifice_flow(area, h) \ No newline at end of file From 73c5da184c75a03990ff5a28e14f0f9483c7895d Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 20:56:33 +0100 Subject: [PATCH 4/9] Refactor argument binding in desugarDef function Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- src/Lang/Desugar.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lang/Desugar.hs b/src/Lang/Desugar.hs index 7e0898f..3c5798e 100644 --- a/src/Lang/Desugar.hs +++ b/src/Lang/Desugar.hs @@ -43,10 +43,11 @@ desugarDef (Return e) = emitDefs [Return e] desugarDef (AnnDef _ _) = return () desugarDef (FunDef id args body) = do bodyExpr <- desugarBody body + argVar <- freshVar let typedArgs = functionArguments args body argType = functionArgType typedArgs - bindArgs = bindFunctionArgs typedArgs (Var "_args") bodyExpr - functionExpr = Abs "_args" (Just argType) bindArgs + bindArgs = bindFunctionArgs typedArgs (Var argVar) bodyExpr + functionExpr = Abs argVar (Just argType) bindArgs emitDefs [ValDef (VarLhs id Nothing) functionExpr] desugarDef (ValDef lhs e) = do desugarVal lhs e From cba096bf0ed62806cb265fa0173de22cba60878e Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 20:58:14 +0100 Subject: [PATCH 5/9] changelog --- changelog.md | 21 +++++++++++++++++++ .../cases/negative/label-conflict.frtl.output | 1 + tests/cases/positive/def-body-annotation.frtl | 7 +++++++ .../positive/def-body-annotation.frtl.output | 1 + tests/cases/positive/def-functions.frtl | 5 +++++ .../cases/positive/def-functions.frtl.output | 1 + 6 files changed, 36 insertions(+) create mode 100644 changelog.md create mode 100644 tests/cases/negative/label-conflict.frtl.output create mode 100644 tests/cases/positive/def-body-annotation.frtl create mode 100644 tests/cases/positive/def-body-annotation.frtl.output create mode 100644 tests/cases/positive/def-functions.frtl create mode 100644 tests/cases/positive/def-functions.frtl.output diff --git a/changelog.md b/changelog.md new file mode 100644 index 0000000..ce1351a --- /dev/null +++ b/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). \ No newline at end of file diff --git a/tests/cases/negative/label-conflict.frtl.output b/tests/cases/negative/label-conflict.frtl.output new file mode 100644 index 0000000..e2e7ed9 --- /dev/null +++ b/tests/cases/negative/label-conflict.frtl.output @@ -0,0 +1 @@ +tests/cases/negative/label-conflict.frtl:2:5: Overlapping descriptor key `Unit` conflicts: Unit[m] vs Unit[s] \ No newline at end of file diff --git a/tests/cases/positive/def-body-annotation.frtl b/tests/cases/positive/def-body-annotation.frtl new file mode 100644 index 0000000..bb55212 --- /dev/null +++ b/tests/cases/positive/def-body-annotation.frtl @@ -0,0 +1,7 @@ +def increment(x): + x : Float[Unit[1]] + result : Float[Unit[1]] + result = x + (1.0 : Float[Unit[1]]) + return result + +it : Float[Unit[1]] = increment((2.0 : Float[Unit[1]])) \ No newline at end of file diff --git a/tests/cases/positive/def-body-annotation.frtl.output b/tests/cases/positive/def-body-annotation.frtl.output new file mode 100644 index 0000000..f398a20 --- /dev/null +++ b/tests/cases/positive/def-body-annotation.frtl.output @@ -0,0 +1 @@ +3.0 \ No newline at end of file diff --git a/tests/cases/positive/def-functions.frtl b/tests/cases/positive/def-functions.frtl new file mode 100644 index 0000000..d3cfeed --- /dev/null +++ b/tests/cases/positive/def-functions.frtl @@ -0,0 +1,5 @@ +def add(x: Float[1], y: Float[1]): + result = x + y + return result + +it : Float[1] = add(2.0, 3.0) \ No newline at end of file diff --git a/tests/cases/positive/def-functions.frtl.output b/tests/cases/positive/def-functions.frtl.output new file mode 100644 index 0000000..6e63660 --- /dev/null +++ b/tests/cases/positive/def-functions.frtl.output @@ -0,0 +1 @@ +5.0 \ No newline at end of file From 5731d94247310b1b4376b1729e98622a4f56b5c1 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 20:58:39 +0100 Subject: [PATCH 6/9] test cases --- examples/coriolis.frtl.output | 1 + examples/diffusion.frtl.output | 1 + examples/flow-rate.frtl.output | 1 + 3 files changed, 3 insertions(+) create mode 100644 examples/coriolis.frtl.output create mode 100644 examples/diffusion.frtl.output create mode 100644 examples/flow-rate.frtl.output diff --git a/examples/coriolis.frtl.output b/examples/coriolis.frtl.output new file mode 100644 index 0000000..4af1832 --- /dev/null +++ b/examples/coriolis.frtl.output @@ -0,0 +1 @@ +None \ No newline at end of file diff --git a/examples/diffusion.frtl.output b/examples/diffusion.frtl.output new file mode 100644 index 0000000..4af1832 --- /dev/null +++ b/examples/diffusion.frtl.output @@ -0,0 +1 @@ +None \ No newline at end of file diff --git a/examples/flow-rate.frtl.output b/examples/flow-rate.frtl.output new file mode 100644 index 0000000..4af1832 --- /dev/null +++ b/examples/flow-rate.frtl.output @@ -0,0 +1 @@ +None \ No newline at end of file From fada8d6ba72f4fb1a7b855a109ea45df9e3fcb7c Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 22:00:02 +0100 Subject: [PATCH 7/9] tidyup --- src/Lang/Desugar.hs | 104 ++++++++++++------ src/Lang/Frontend.hs | 36 +++--- src/Lang/Parser.y | 4 +- src/Lang/Primitives.hs | 2 + src/Lang/TypeError.hs | 8 ++ src/Lang/Types.hs | 7 ++ .../duplicate-parameter-annotation.frtl | 5 + ...duplicate-parameter-annotation.frtl.output | 1 + .../missing-parameter-annotation.frtl | 4 + .../missing-parameter-annotation.frtl.output | 1 + 10 files changed, 123 insertions(+), 49 deletions(-) create mode 100644 tests/cases/negative/duplicate-parameter-annotation.frtl create mode 100644 tests/cases/negative/duplicate-parameter-annotation.frtl.output create mode 100644 tests/cases/negative/missing-parameter-annotation.frtl create mode 100644 tests/cases/negative/missing-parameter-annotation.frtl.output diff --git a/src/Lang/Desugar.hs b/src/Lang/Desugar.hs index 3c5798e..bb37bcb 100644 --- a/src/Lang/Desugar.hs +++ b/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,31 +34,39 @@ 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 (AnnDef _ _) = return () +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 - bodyExpr <- desugarBody body - argVar <- freshVar - let typedArgs = functionArguments args body - argType = functionArgType typedArgs - bindArgs = bindFunctionArgs typedArgs (Var argVar) bodyExpr - functionExpr = Abs argVar (Just argType) bindArgs - emitDefs [ValDef (VarLhs id Nothing) functionExpr] -desugarDef (ValDef lhs e) = do desugarVal lhs e + 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 @@ -58,28 +75,49 @@ desugarDef (ValDef lhs e) = do desugarVal lhs e -- 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. -functionArguments :: [(Identifier, Maybe (Type 0))] -> [Def 'Parsed] -> [(Identifier, Type 0)] -functionArguments args body = map argumentType args +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:_ -> (arg, ty) + ty:_ | Just _ <- headerType -> + Left $ WellFormednessError $ DuplicateParameterAnnotation arg + ty:_ -> Right (arg, ty) [] -> case headerType of - Just ty -> (arg, ty) - Nothing -> error $ "Missing type annotation for function parameter " ++ arg + 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 [( _, ty)] = ty +functionArgType [] = tyCon0 "()" functionArgType args = foldr1 ProdTy (map snd args) -desugarBody :: [Def 'Parsed] -> Desugar Expr -desugarBody [] = return (Con "None" []) -desugarBody (Return e : _) = return e -desugarBody (AnnDef _ _ : defs) = desugarBody defs -desugarBody (ValDef lhs e : defs) = do - rest <- desugarBody defs - bindLhs lhs e rest -desugarBody (_ : defs) = desugarBody defs +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) diff --git a/src/Lang/Frontend.hs b/src/Lang/Frontend.hs index 38901bb..416d449 100644 --- a/src/Lang/Frontend.hs +++ b/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 diff --git a/src/Lang/Parser.y b/src/Lang/Parser.y index 2b97f07..76d1a66 100644 --- a/src/Lang/Parser.y +++ b/src/Lang/Parser.y @@ -242,7 +242,8 @@ NumFloat TypeAtom :: { [Option] -> Type 0 } TypeAtom - : IDENT { \opts -> tyCon0 $ symString $1 } + : '(' ')' { \_ -> tyCon0 "()" } + | IDENT { \opts -> tyCon0 $ symString $1 } | TYVAR { \opts -> TyVar $ tyVarString $1 } | '(' Type ')' { \opts -> $2 opts } | INT { \opts -> tyCon0 $ let (TokenInt _ x) = $1 in x } @@ -250,6 +251,7 @@ TypeAtom Juxt :: { [Option] -> Expr } : Juxt '(' Expr ')' { \opts -> App ($1 opts) ($3 opts) } + | Juxt '(' ')' { \opts -> App ($1 opts) (Con "()" []) } | cast '(' Atom ')' { \opts -> MkCast (mkPos $1) ($3 opts) } | Atom { $1 } diff --git a/src/Lang/Primitives.hs b/src/Lang/Primitives.hs index 2df95ea..93b3251 100644 --- a/src/Lang/Primitives.hs +++ b/src/Lang/Primitives.hs @@ -36,6 +36,7 @@ desc2 = tyCon2 "Descriptor" dataConstructors :: [(Identifier, Type 0)] dataConstructors = [ ("None" , tyCon0 "None") + , ("()" , tyCon0 "()") , ("True" , boolTy (tyCon0 "1")) , ("False" , boolTy (tyCon0 "1")) ] @@ -51,6 +52,7 @@ typeConstructors = [ -- Graded boolean , ("Bool" , ImplicitFunTy "d" desc2 (FunTy (tyVar "d") type0)) , ("Nat" , type0) + , ("()" , type0) , ("Unit" , FunTy type0 (tyCon1 "UoM")) , ("Quantity" , FunTy type0 (tyCon1 "KoQ")) , ("Species" , FunTy type0 (tyCon1 "SpeciesType")) diff --git a/src/Lang/TypeError.hs b/src/Lang/TypeError.hs index 82626cc..59cd437 100644 --- a/src/Lang/TypeError.hs +++ b/src/Lang/TypeError.hs @@ -55,6 +55,9 @@ data TypeError | FreeVariablesInAbstraction [Identifier] | TermLevelTypeAbstraction Identifier | TypeApplicationExpectsType + + -- Program well-formedness errors + | WellFormednessError WellFormednessError -- Generic/contextual errors | ContextualError String @@ -67,6 +70,11 @@ data TypeError deriving (Show) +data WellFormednessError + = MissingParameterAnnotation Identifier + | DuplicateParameterAnnotation Identifier + deriving (Show) + class MonadAlt m where (<|>) :: m a -> m a -> m a diff --git a/src/Lang/Types.hs b/src/Lang/Types.hs index 50bca02..a07e1b9 100644 --- a/src/Lang/Types.hs +++ b/src/Lang/Types.hs @@ -726,6 +726,13 @@ errorToString (TermLevelTypeAbstraction alpha) = errorToString TypeApplicationExpectsType = "Type application expects a type" +errorToString (WellFormednessError err) = + "Malformed program: " <> case err of + MissingParameterAnnotation parameter -> + "function parameter `" <> parameter <> "` has no type annotation" + DuplicateParameterAnnotation parameter -> + "function parameter `" <> parameter <> "` is annotated in both the header and body" + errorToString (ContextualError msg) = msg diff --git a/tests/cases/negative/duplicate-parameter-annotation.frtl b/tests/cases/negative/duplicate-parameter-annotation.frtl new file mode 100644 index 0000000..a903ce5 --- /dev/null +++ b/tests/cases/negative/duplicate-parameter-annotation.frtl @@ -0,0 +1,5 @@ +def identity(x: Float[Unit[1]]): + x : Float[Unit[1]] + return x + +it = identity((1.0 : Float[Unit[1]])) \ No newline at end of file diff --git a/tests/cases/negative/duplicate-parameter-annotation.frtl.output b/tests/cases/negative/duplicate-parameter-annotation.frtl.output new file mode 100644 index 0000000..3d00c64 --- /dev/null +++ b/tests/cases/negative/duplicate-parameter-annotation.frtl.output @@ -0,0 +1 @@ +Malformed program: function parameter `x` is annotated in both the header and body \ No newline at end of file diff --git a/tests/cases/negative/missing-parameter-annotation.frtl b/tests/cases/negative/missing-parameter-annotation.frtl new file mode 100644 index 0000000..fcea1dc --- /dev/null +++ b/tests/cases/negative/missing-parameter-annotation.frtl @@ -0,0 +1,4 @@ +def identity(x): + return x + +it = identity(1.0) \ No newline at end of file diff --git a/tests/cases/negative/missing-parameter-annotation.frtl.output b/tests/cases/negative/missing-parameter-annotation.frtl.output new file mode 100644 index 0000000..b9b0ab6 --- /dev/null +++ b/tests/cases/negative/missing-parameter-annotation.frtl.output @@ -0,0 +1 @@ +Malformed program: function parameter `x` has no type annotation \ No newline at end of file From 27e6eba46c6fb0125eebb50c2608953f34d108d7 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 22:01:43 +0100 Subject: [PATCH 8/9] synthesis type of unit --- examples/flow-rate.frtl.output | 2 +- src/Lang/Types.hs | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/examples/flow-rate.frtl.output b/examples/flow-rate.frtl.output index 4af1832..6d5a64b 100644 --- a/examples/flow-rate.frtl.output +++ b/examples/flow-rate.frtl.output @@ -1 +1 @@ -None \ No newline at end of file +60.406948 \ No newline at end of file diff --git a/src/Lang/Types.hs b/src/Lang/Types.hs index a07e1b9..131560e 100644 --- a/src/Lang/Types.hs +++ b/src/Lang/Types.hs @@ -280,6 +280,8 @@ synth_ gamma (Var x) = Just ty -> Right ty Nothing -> Left $ VariableNotFound x +synth_ _ (Con "()" []) = Right $ tyCon0 "()" + synth_ gamma (Let x e1 e2) = do ty1 <- synth gamma e1 synth ((x, ty1) : gamma) e2 From 5f23ce72b0a935889f1c1e247d7b150e98589a83 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Sat, 5 Sep 2026 21:58:03 +0100 Subject: [PATCH 9/9] empty tuple and typing --- src/Lang/Parser.y | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lang/Parser.y b/src/Lang/Parser.y index 76d1a66..bf41b85 100644 --- a/src/Lang/Parser.y +++ b/src/Lang/Parser.y @@ -256,7 +256,8 @@ Juxt :: { [Option] -> Expr } | Atom { $1 } Atom :: { [Option] -> Expr } - : '(' Expr ')' { $2 } + : '(' ')' { \_ -> Con "()" [] } + | '(' Expr ')' { $2 } | IDENT { \opts -> MkVar (mkPos $1) (symString $1) } | LAMBDA IDENT ':' Expr { \opts -> MkAbs (mkPos $1) (symString $2) Nothing ($4 opts) }