Explicit local bindings for let/where

src/Check/Core.hs

@@ -165,6 +165,9 @@ definitionUnsafeBaseReason localNames allowedExternalFacts bound ast = case ast
   TStem _ -> Just "uses raw t directly"
   TFork _ _ -> Just "uses raw t directly"
   SLambda args body -> definitionUnsafeBaseReason localNames allowedExternalFacts (foldr Set.insert bound args) body
+  SLet name val body ->
+    definitionUnsafeBaseReason localNames allowedExternalFacts bound val
+      <|> definitionUnsafeBaseReason localNames allowedExternalFacts (Set.insert name bound) body
   SEmpty -> Nothing
   SImport _ _ -> Nothing
 
@@ -187,6 +190,7 @@ astFreeRefs candidates ast = case ast of
   TStem inner -> astFreeRefs candidates inner
   TFork left right -> astFreeRefs candidates left ++ astFreeRefs candidates right
   SLambda args body -> astFreeRefs (foldr Set.delete candidates args) body
+  SLet name val body -> astFreeRefs candidates val ++ astFreeRefs (Set.delete name candidates) body
   SEmpty -> []
   SImport _ _ -> []
 
@@ -584,6 +588,14 @@ lowerExprKnownAgainst expr expected = case (expr, viewExprAsType expected) of
   (SApp (SApp (SVar "err" _) value) rest, Just (VTResult errView _)) ->
     lowerUnshadowedConstructor "err" expr expected $
       lowerResultConstructor expected (viewTypeToExpr errView) value rest
+  (SLet name value body, _) -> do
+    (valueSym, valueNodes, _) <- lowerExprKnown value
+    recordDebugName valueSym name
+    bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
+    let (bodySym, bodyNodes, bodyKnown) = bodyResult
+    pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
+  -- Hand-written immediately-applied lambda (not compiler output; let/where
+  -- now emit SLet). Kept for source that relies on alias semantics.
   (SApp (SLambda [name] body) value, _) -> do
     (valueSym, valueNodes, _) <- lowerExprKnown value
     bodyResult <- withLocalAlias name valueSym (lowerExprKnownAgainst body expected)
@@ -658,6 +670,14 @@ lowerExprKnown TLeaf = do
 lowerExprKnown (SList items) = do
   (sym, nodes, view, _) <- lowerListLiteral items
   pure (sym, nodes, Just view)
+lowerExprKnown (SLet name value body) = do
+  (valueSym, valueNodes, _) <- lowerExprKnown value
+  recordDebugName valueSym name
+  bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)
+  let (bodySym, bodyNodes, bodyKnown) = bodyResult
+  pure (bodySym, valueNodes ++ bodyNodes, bodyKnown)
+-- Hand-written immediately-applied lambda (not compiler output; let/where
+-- now emit SLet). Kept for source that relies on alias semantics.
 lowerExprKnown (SApp (SLambda [name] body) value) = do
   (valueSym, valueNodes, known) <- lowerExprKnown value
   bodyResult <- withLocalAlias name valueSym (lowerExprKnown body)

src/Check/IO.hs

@@ -105,6 +105,7 @@ instrumentIOContinuations asts = mapM transformTop asts
       SApp (SVar "io" h) action -> SApp (SVar "io" h) <$> transformIOAction action
       SApp f a -> SApp <$> transformExpr f <*> transformExpr a
       SLambda params body -> SLambda params <$> transformExpr body
+      SLet name val body -> SLet name <$> transformExpr val <*> transformExpr body
       TStem x -> TStem <$> transformExpr x
       TFork x y -> TFork <$> transformExpr x <*> transformExpr y
       _ -> pure expr
@@ -118,6 +119,7 @@ instrumentIOContinuations asts = mapM transformTop asts
         SApp <$> (SApp (SVar "bind" h) <$> transformIOAction left) <*> (SLambda params <$> transformIOAction body)
       SApp f a -> SApp <$> transformIOAction f <*> transformIOAction a
       SLambda params body -> SLambda params <$> transformIOAction body
+      SLet name val body -> SLet name <$> transformIOAction val <*> transformIOAction body
       _ -> transformExpr action
 
     checkedPureActionFor value =
@@ -183,6 +185,7 @@ mentionsContractedName contracts expr = case expr of
   SVar name _ -> Map.member name contracts
   SApp f a -> mentionsContractedName contracts f || mentionsContractedName contracts a
   SLambda _ body -> mentionsContractedName contracts body
+  SLet _ val body -> mentionsContractedName contracts val || mentionsContractedName contracts body
   SList items -> any (mentionsContractedName contracts) items
   TStem x -> mentionsContractedName contracts x
   TFork x y -> mentionsContractedName contracts x || mentionsContractedName contracts y
@@ -372,6 +375,7 @@ substAst subst expr = case expr of
   SVar name Nothing -> Map.findWithDefault expr name subst
   SApp f a -> SApp (substAst subst f) (substAst subst a)
   SLambda params body -> SLambda params (substAst (foldr Map.delete subst params) body)
+  SLet name val body -> SLet name (substAst subst val) (substAst (Map.delete name subst) body)
   SList items -> SList (map (substAst subst) items)
   TStem x -> TStem (substAst subst x)
   TFork x y -> TFork (substAst subst x) (substAst subst y)
@@ -397,6 +401,7 @@ astSource expr = case expr of
   SList items -> "[" ++ unwords (map (parens . astSource) items) ++ "]"
   SApp f a -> parens (astSource f) ++ " " ++ parens (astSource a)
   SLambda params body -> parens (unwords params ++ " : " ++ astSource body)
+  SLet name val body -> parens ("let " ++ name ++ " = " ++ astSource val ++ " in " ++ astSource body)
   TLeaf -> "t"
   TStem x -> "(t " ++ astSource x ++ ")"
   TFork x y -> "(t " ++ astSource x ++ " " ++ astSource y ++ ")"

src/Eval.hs

@@ -75,6 +75,7 @@ evalTricu env x = go env (reorderDefs env (map recoverParams x))
 evalASTSync :: Env -> TricuAST -> T
 evalASTSync env term = case term of
   SLambda _ _ -> evalASTSync env (elimLambda term)
+  SLet name val body -> evalASTSync env (SApp (SLambda [name] body) val)
   SVar name Nothing -> case Map.lookup name env of
     Just v -> v
     Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined"
@@ -108,6 +109,7 @@ annotatedBinders (DefPhantom _ : rest) = annotatedBinders rest
 elimLambda :: TricuAST -> TricuAST
 elimLambda = go
   where
+    go (SLet name val body) = go (SApp (SLambda [name] body) val)
     go term
       | etaReduction term   = go (etaReduceResult term)
       | triagePattern term  = _TRI
@@ -190,6 +192,8 @@ freeVars (SVar v Nothing) = Set.singleton v
 freeVars (SVar v (Just _)) = Set.singleton v
 freeVars (SApp t u) = Set.union (freeVars t) (freeVars u)
 freeVars (SLambda vs body) = Set.difference (freeVars body) (Set.fromList vs)
+freeVars (SLet name val body) =
+  Set.union (freeVars val) (Set.delete name (freeVars body))
 freeVars (SDef _ params body) = Set.difference (freeVars body) (Set.fromList params)
 freeVars (SDefAnn _ args _ body) = Set.difference (freeVars body) (Set.fromList (annotatedBinders args))
 freeVars (TStem t) = freeVars t
@@ -297,6 +301,7 @@ findVarNames ast = case ast of
   SVar name _ -> [name]
   SApp a b -> findVarNames a ++ findVarNames b
   SLambda args body -> findVarNames body \\ args
+  SLet name val body -> findVarNames val ++ (findVarNames body \\ [name])
   SDef name args body -> name : (findVarNames body \\ args)
   SDefAnn name args _ body -> name : (findVarNames body \\ annotatedBinders args)
   _ -> []
@@ -317,6 +322,7 @@ toDB env = \case
   SInt n       -> BInt n
   SList xs     -> BList (map (toDB env) xs)
   SEmpty       -> BEmpty
+  SLet name val body -> toDB env (SApp (SLambda [name] body) val)
   SDef{}       -> error "toDB: unexpected SDef at this stage"
   SDefAnn{}    -> error "toDB: unexpected SDefAnn at this stage"
   SImport _ _  -> BEmpty

src/Parser.hs

@@ -496,7 +496,7 @@ whereChainP parseBody = do
     Nothing -> pure body
     Just (name, args, value) ->
       let boundValue = foldr (\p acc -> SLambda [p] acc) value args
-      in pure (SApp (SLambda [name] body) boundValue)
+      in pure (SLet name boundValue body)
 
 whereBindingP :: TokParser (String, [String], TricuAST)
 whereBindingP = do
@@ -524,7 +524,7 @@ letP = do
   bodyIndent <- skipNestedNewlinesGetIndent
   body <- exprAtIndentP bodyIndent
   let boundValue = foldr (\p acc -> SLambda [p] acc) value args
-  pure (SApp (SLambda [name] body) boundValue)
+  pure (SLet name boundValue body)
 
 data DoStmt
   = DoBind String TricuAST

src/Research.hs

@@ -84,6 +84,11 @@ data TricuAST
   | TStem TricuAST
   | TFork TricuAST TricuAST
   | SLambda [String] TricuAST
+  -- Non-recursive local binding: `name = boundValue` scoped over `body`.
+  -- Produced by let/where desugaring. `boundValue` already folds any binding
+  -- arguments into nested SLambda. Semantically equal to
+  --   SApp (SLambda [name] body) boundValue
+  | SLet String TricuAST TricuAST
   | SEmpty
   | SImport String String
   deriving (Show, Eq, Ord)

test/Spec.hs

@@ -336,7 +336,7 @@ parser = testGroup "Parser Tests"
 
   , testCase "Parse let expression" $ do
       let input  = "let x = t t in x"
-          expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf)
+          expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing)
       parseSingle input @?= expect
 
   , testCase "Evaluate let expression" $ do
@@ -344,18 +344,36 @@ parser = testGroup "Parser Tests"
 
   , testCase "Parse let function binding" $ do
       let input  = "let f x = x in f t"
-          expect = SApp (SLambda ["f"] (SApp (SVar "f" Nothing) TLeaf))
+          expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing))
-                        (SLambda ["x"] (SVar "x" Nothing))
+                        (SApp (SVar "f" Nothing) TLeaf)
       parseSingle input @?= expect
 
   , testCase "Parse where expression" $ do
       let input  = "x where x = t t"
-          expect = SApp (SLambda ["x"] (SVar "x" Nothing)) (SApp TLeaf TLeaf)
+          expect = SLet "x" (SApp TLeaf TLeaf) (SVar "x" Nothing)
       parseSingle input @?= expect
 
   , testCase "Evaluate where expression" $ do
       tricuTestString "x where x = 1" @?= "Fork (Stem Leaf) Leaf"
 
+  , testCase "Parse where binding with arguments (SLet)" $ do
+      let input  = "f 3 where f x = x"
+          expect = SLet "f" (SLambda ["x"] (SVar "x" Nothing))
+                        (SApp (SVar "f" Nothing) (SInt 3))
+      parseSingle input @?= expect
+
+  , testCase "Evaluate where binding with arguments matches applied lambda" $ do
+      tricuTestString "f (t t) where f x = t x x"
+        @?= tricuTestString "(f : f (t t)) (x : t x x)"
+
+  , testCase "Evaluate nested let bindings" $ do
+      tricuTestString "let a = t t in let b = t in t a b"
+        @?= tricuTestString "t (t t) t"
+
+  , testCase "Inner let binding shadows outer binding" $ do
+      tricuTestString "let x = t in let x = t t in x"
+        @?= tricuTestString "t t"
+
   , testCase "Parse indented multiline definition body" $ do
       let input  = "x =\n  t\n    t"
           expect = SDef "x" [] (SApp TLeaf TLeaf)