Named arguments syntax with function definitions (#2494)

* Closes #2365 * Implements the syntax `f@{x1 := def1; ...; xn := defn}` and `f@?{x1 := def1; ..; xn := defn}`. Each definition inside the `@{..}` is an ordinary function definition. The `@?` version allows partial application (not all explicit named arguments need to be provided). This subsumes the old record creation syntax.
2024-09-11 16:26:33 +03:00 · 2023-11-07 12:02:22 +01:00 · 2023-11-07 12:02:22 +01:00 · 5948a38a54
commit 5948a38a54
parent 9690aadf53
17 changed files with 308 additions and 215 deletions
--- a/src/Juvix/Compiler/Concrete/Keywords.hs
+++ b/src/Juvix/Compiler/Concrete/Keywords.hs
@ -27,6 +27,7 @@ import Juvix.Data.Keyword.All
    kwAssign,
    kwAssoc,
    kwAt,
+    kwAtQuestion,
    kwAxiom,
    kwBelow,
    kwBinary,
@ -82,6 +83,7 @@ reservedKeywords =
  [ delimSemicolon,
    kwAssign,
    kwAt,
+    kwAtQuestion,
    kwAxiom,
    kwCase,
    kwColon,
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@ -54,11 +54,6 @@ type family RecordUpdateExtraType s = res | res -> s where
  RecordUpdateExtraType 'Parsed = ()
  RecordUpdateExtraType 'Scoped = RecordUpdateExtra

-type RecordCreationExtraType :: Stage -> GHC.Type
-type family RecordCreationExtraType s = res | res -> s where
-  RecordCreationExtraType 'Parsed = ()
-  RecordCreationExtraType 'Scoped = RecordCreationExtra
-
 type FieldArgIxType :: Stage -> GHC.Type
 type family FieldArgIxType s = res | res -> s where
  FieldArgIxType 'Parsed = ()
@ -576,23 +571,6 @@ deriving stock instance Ord (RecordUpdateField 'Parsed)

 deriving stock instance Ord (RecordUpdateField 'Scoped)

-data RecordDefineField (s :: Stage) = RecordDefineField
-  { _fieldDefineFunDef :: FunctionDef s,
-    _fieldDefineIden :: IdentifierType s
-  }
-
-deriving stock instance Show (RecordDefineField 'Parsed)
-
-deriving stock instance Show (RecordDefineField 'Scoped)
-
-deriving stock instance Eq (RecordDefineField 'Parsed)
-
-deriving stock instance Eq (RecordDefineField 'Scoped)
-
-deriving stock instance Ord (RecordDefineField 'Parsed)
-
-deriving stock instance Ord (RecordDefineField 'Scoped)
-
 data RecordField (s :: Stage) = RecordField
  { _fieldName :: SymbolType s,
    _fieldColon :: Irrelevant (KeywordRef),
@ -1217,7 +1195,7 @@ data Expression
  | ExpressionDoubleBraces (DoubleBracesExpression 'Scoped)
  | ExpressionIterator (Iterator 'Scoped)
  | ExpressionNamedApplication (NamedApplication 'Scoped)
-  | ExpressionRecordCreation (RecordCreation 'Scoped)
+  | ExpressionNamedApplicationNew (NamedApplicationNew 'Scoped)
  deriving stock (Show, Eq, Ord)

 data DoubleBracesExpression (s :: Stage) = DoubleBracesExpression
@ -1585,11 +1563,6 @@ data RecordUpdateExtra = RecordUpdateExtra
    _recordUpdateExtraVars :: [S.Symbol]
  }

-newtype RecordCreationExtra = RecordCreationExtra
-  { -- | Implicitly bound fields sorted by index
-    _recordCreationExtraVars :: [S.Symbol]
-  }
-
 newtype ParensRecordUpdate = ParensRecordUpdate
  { _parensRecordUpdate :: RecordUpdate 'Scoped
  }
@ -1638,6 +1611,41 @@ deriving stock instance Ord (NamedApplication 'Parsed)

 deriving stock instance Ord (NamedApplication 'Scoped)

+newtype NamedArgumentNew (s :: Stage) = NamedArgumentNew
+  { _namedArgumentNewFunDef :: FunctionDef s
+  }
+
+deriving stock instance Show (NamedArgumentNew 'Parsed)
+
+deriving stock instance Show (NamedArgumentNew 'Scoped)
+
+deriving stock instance Eq (NamedArgumentNew 'Parsed)
+
+deriving stock instance Eq (NamedArgumentNew 'Scoped)
+
+deriving stock instance Ord (NamedArgumentNew 'Parsed)
+
+deriving stock instance Ord (NamedArgumentNew 'Scoped)
+
+data NamedApplicationNew (s :: Stage) = NamedApplicationNew
+  { _namedApplicationNewName :: IdentifierType s,
+    _namedApplicationNewAtKw :: Irrelevant KeywordRef,
+    _namedApplicationNewExhaustive :: Bool,
+    _namedApplicationNewArguments :: [NamedArgumentNew s]
+  }
+
+deriving stock instance Show (NamedApplicationNew 'Parsed)
+
+deriving stock instance Show (NamedApplicationNew 'Scoped)
+
+deriving stock instance Eq (NamedApplicationNew 'Parsed)
+
+deriving stock instance Eq (NamedApplicationNew 'Scoped)
+
+deriving stock instance Ord (NamedApplicationNew 'Parsed)
+
+deriving stock instance Ord (NamedApplicationNew 'Scoped)
+
 data RecordStatement (s :: Stage)
  = RecordStatementField (RecordField s)
  | RecordStatementOperator OperatorSyntaxDef
@ -1654,25 +1662,6 @@ deriving stock instance Ord (RecordStatement 'Parsed)

 deriving stock instance Ord (RecordStatement 'Scoped)

-data RecordCreation (s :: Stage) = RecordCreation
-  { _recordCreationConstructor :: IdentifierType s,
-    _recordCreationAtKw :: Irrelevant KeywordRef,
-    _recordCreationFields :: [RecordDefineField s],
-    _recordCreationExtra :: Irrelevant (RecordCreationExtraType s)
-  }
-
-deriving stock instance Show (RecordCreation 'Parsed)
-
-deriving stock instance Show (RecordCreation 'Scoped)
-
-deriving stock instance Eq (RecordCreation 'Parsed)
-
-deriving stock instance Eq (RecordCreation 'Scoped)
-
-deriving stock instance Ord (RecordCreation 'Parsed)
-
-deriving stock instance Ord (RecordCreation 'Scoped)
-
 -- | Expressions without application
 data ExpressionAtom (s :: Stage)
  = AtomIdentifier (IdentifierType s)
@ -1693,7 +1682,7 @@ data ExpressionAtom (s :: Stage)
  | AtomParens (ExpressionType s)
  | AtomIterator (Iterator s)
  | AtomNamedApplication (NamedApplication s)
-  | AtomRecordCreation (RecordCreation s)
+  | AtomNamedApplicationNew (NamedApplicationNew s)

 deriving stock instance Show (ExpressionAtom 'Parsed)

@ -1855,11 +1844,9 @@ makeLenses ''RecordPatternAssign
 makeLenses ''RecordPattern
 makeLenses ''ParensRecordUpdate
 makeLenses ''RecordUpdateExtra
-makeLenses ''RecordCreationExtra
 makeLenses ''RecordUpdate
 makeLenses ''RecordUpdateApp
 makeLenses ''RecordUpdateField
-makeLenses ''RecordDefineField
 makeLenses ''NonDefinitionsSection
 makeLenses ''DefinitionsSection
 makeLenses ''ProjectionDef
@ -1924,6 +1911,8 @@ makeLenses ''ModuleIndex
 makeLenses ''ArgumentBlock
 makeLenses ''NamedArgument
 makeLenses ''NamedApplication
+makeLenses ''NamedArgumentNew
+makeLenses ''NamedApplicationNew
 makeLenses ''AliasDef
 makeLenses ''FixitySyntaxDef
 makeLenses ''ParsedFixityInfo
@ -1991,7 +1980,7 @@ instance HasAtomicity (ArgumentBlock s) where
 instance HasAtomicity (NamedApplication s) where
  atomicity = const (Aggregate appFixity)

-instance HasAtomicity (RecordCreation s) where
+instance HasAtomicity (NamedApplicationNew s) where
  atomicity = const (Aggregate updateFixity)

 instance HasAtomicity Expression where
@ -2015,7 +2004,7 @@ instance HasAtomicity Expression where
    ExpressionNewCase c -> atomicity c
    ExpressionIterator i -> atomicity i
    ExpressionNamedApplication i -> atomicity i
-    ExpressionRecordCreation i -> atomicity i
+    ExpressionNamedApplicationNew i -> atomicity i
    ExpressionRecordUpdate {} -> Aggregate updateFixity
    ExpressionParensRecordUpdate {} -> Atom

@ -2145,19 +2134,15 @@ instance HasLoc (List s) where
 instance (SingI s) => HasLoc (NamedApplication s) where
  getLoc NamedApplication {..} = getLocIdentifierType _namedAppName <> getLoc (last _namedAppArgs)

+instance (SingI s) => HasLoc (NamedApplicationNew s) where
+  getLoc NamedApplicationNew {..} = getLocIdentifierType _namedApplicationNewName
+
 instance (SingI s) => HasLoc (RecordUpdateField s) where
  getLoc f = getLocSymbolType (f ^. fieldUpdateName) <> getLocExpressionType (f ^. fieldUpdateValue)

-instance (SingI s) => HasLoc (RecordDefineField s) where
-  getLoc f = getLoc (f ^. fieldDefineFunDef)
-
 instance HasLoc (RecordUpdate s) where
  getLoc r = getLoc (r ^. recordUpdateAtKw) <> getLoc (r ^. recordUpdateDelims . unIrrelevant . _2)

-- TODO add delims
-instance (SingI s) => HasLoc (RecordCreation s) where
-  getLoc RecordCreation {..} = getLocIdentifierType _recordCreationConstructor
-
 instance HasLoc RecordUpdateApp where
  getLoc r = getLoc (r ^. recordAppExpression) <> getLoc (r ^. recordAppUpdate)

@ -2193,7 +2178,7 @@ instance HasLoc Expression where
    ExpressionDoubleBraces i -> getLoc i
    ExpressionIterator i -> getLoc i
    ExpressionNamedApplication i -> getLoc i
-    ExpressionRecordCreation i -> getLoc i
+    ExpressionNamedApplicationNew i -> getLoc i
    ExpressionRecordUpdate i -> getLoc i
    ExpressionParensRecordUpdate i -> getLoc i

@ -2485,13 +2470,12 @@ instance (SingI s) => IsApe (NamedApplication s) ApeLeaf where
    where
      f = toApeIdentifierType _namedAppName

-instance (SingI s) => IsApe (RecordCreation s) ApeLeaf where
-  toApe :: RecordCreation s -> Ape ApeLeaf
+instance (SingI s) => IsApe (NamedApplicationNew s) ApeLeaf where
  toApe a =
    ApeLeaf $
      Leaf
        { _leafAtomicity = atomicity a,
-          _leafExpr = ApeLeafAtom (sing :&: AtomRecordCreation a)
+          _leafExpr = ApeLeafAtom (sing :&: AtomNamedApplicationNew a)
        }

 instance IsApe Application ApeLeaf where
@ -2550,7 +2534,7 @@ instance IsApe Expression ApeLeaf where
    ExpressionPostfixApplication a -> toApe a
    ExpressionFunction a -> toApe a
    ExpressionNamedApplication a -> toApe a
-    ExpressionRecordCreation a -> toApe a
+    ExpressionNamedApplicationNew a -> toApe a
    ExpressionRecordUpdate a -> toApe a
    ExpressionParensRecordUpdate {} -> leaf
    ExpressionParensIdentifier {} -> leaf
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@ -290,35 +290,34 @@ instance (SingI s) => PrettyPrint (ArgumentBlock s) where
      Irrelevant d = _argBlockDelims

 instance (SingI s) => PrettyPrint (NamedApplication s) where
-  -- ppCode :: Members '[ExactPrint, Reader Options] r => NamedApplication s -> Sem r ()
  ppCode = apeHelper

+instance (SingI s) => PrettyPrint (NamedApplicationNew s) where
+  ppCode NamedApplicationNew {..} = do
+    let args'
+          | null _namedApplicationNewArguments = mempty
+          | otherwise =
+              blockIndent
+                ( sequenceWith
+                    (semicolon >> line)
+                    (ppCode <$> _namedApplicationNewArguments)
+                )
+    ppIdentifierType _namedApplicationNewName
+      <> ppCode _namedApplicationNewAtKw
+      <> braces args'
+
+instance (SingI s) => PrettyPrint (NamedArgumentNew s) where
+  ppCode NamedArgumentNew {..} = ppCode _namedArgumentNewFunDef
+
 instance (SingI s) => PrettyPrint (RecordStatement s) where
  ppCode = \case
    RecordStatementField f -> ppCode f
    RecordStatementOperator f -> ppCode f

-instance (SingI s) => PrettyPrint (RecordCreation s) where
-  ppCode RecordCreation {..} = do
-    let fields'
-          | null _recordCreationFields = mempty
-          | otherwise =
-              blockIndent
-                ( sequenceWith
-                    (semicolon >> line)
-                    (ppCode <$> _recordCreationFields)
-                )
-    ppIdentifierType _recordCreationConstructor
-      <> ppCode _recordCreationAtKw
-      <> braces fields'
-
 instance (SingI s) => PrettyPrint (RecordUpdateField s) where
  ppCode RecordUpdateField {..} =
    ppSymbolType _fieldUpdateName <+> ppCode _fieldUpdateAssignKw <+> ppExpressionType _fieldUpdateValue

-instance (SingI s) => PrettyPrint (RecordDefineField s) where
-  ppCode RecordDefineField {..} = ppCode _fieldDefineFunDef
-
 instance (SingI s) => PrettyPrint (RecordUpdate s) where
  ppCode RecordUpdate {..} = do
    let Irrelevant (l, r) = _recordUpdateDelims
@ -363,7 +362,7 @@ instance (SingI s) => PrettyPrint (ExpressionAtom s) where
    AtomInstanceHole w -> ppHoleType w
    AtomIterator i -> ppCode i
    AtomNamedApplication i -> ppCode i
-    AtomRecordCreation i -> ppCode i
+    AtomNamedApplicationNew i -> ppCode i

 instance PrettyPrint PatternScopedIden where
  ppCode = \case
@ -800,7 +799,7 @@ instance PrettyPrint Expression where
    ExpressionNewCase c -> ppCode c
    ExpressionIterator i -> ppCode i
    ExpressionNamedApplication i -> ppCode i
-    ExpressionRecordCreation i -> ppCode i
+    ExpressionNamedApplicationNew i -> ppCode i
    ExpressionRecordUpdate i -> ppCode i
    ExpressionParensRecordUpdate i -> ppCode i

--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@ -2153,59 +2153,44 @@ checkExpressionAtom e = case e of
  AtomList l -> pure . AtomList <$> checkList l
  AtomIterator i -> pure . AtomIterator <$> checkIterator i
  AtomNamedApplication i -> pure . AtomNamedApplication <$> checkNamedApplication i
-  AtomRecordCreation i -> pure . AtomRecordCreation <$> checkRecordCreation i
+  AtomNamedApplicationNew i -> pure . AtomNamedApplicationNew <$> checkNamedApplicationNew i
  AtomRecordUpdate i -> pure . AtomRecordUpdate <$> checkRecordUpdate i

-checkRecordCreation :: forall r. (Members '[Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, NameIdGen] r) => RecordCreation 'Parsed -> Sem r (RecordCreation 'Scoped)
-checkRecordCreation RecordCreation {..} = do
-  constrIden <- getNameOfKind KNameConstructor _recordCreationConstructor
-  let cname = constrIden ^. scopedIdenFinal
-  tab <- getInfoTable
-  let mci = HashMap.lookup (cname ^. S.nameId) (tab ^. infoConstructors)
-  case mci of
-    Nothing ->
-      throw (ErrNotAConstructor (NotAConstructor (cname ^. nameConcrete)))
-    Just ci -> do
-      let name = NameUnqualified (ci ^. constructorInfoTypeName . nameConcrete)
-          nameId = ci ^. constructorInfoTypeName . S.nameId
-      info <- getRecordInfo' (getLoc _recordCreationConstructor) name nameId
-      let sig = info ^. recordInfoSignature
-      (vars', fields') <- withLocalScope . localBindings . ignoreSyntax $ do
-        vs <- mapM (reserveFunctionSymbol . (^. fieldDefineFunDef)) _recordCreationFields
-        fs <- mapM (checkDefineField sig) _recordCreationFields
-        return (vs, fs)
-      let extra' =
-            RecordCreationExtra
-              { _recordCreationExtraVars = vars'
-              }
-          snames = HashSet.fromList (HashMap.keys (sig ^. recordNames))
-          sfields = HashSet.fromList (map (^. fieldDefineFunDef . signName . nameConcrete) (toList fields'))
-          missingFields = HashSet.difference snames sfields
-      unless (null missingFields) $
-        throw (ErrMissingFields (MissingFields (cname ^. nameConcrete) missingFields))
-      return
-        RecordCreation
-          { _recordCreationConstructor = constrIden,
-            _recordCreationFields = fields',
-            _recordCreationExtra = Irrelevant extra',
-            _recordCreationAtKw
-          }
-
-checkDefineField ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, NameIdGen] r) =>
-  RecordNameSignature 'Parsed ->
-  RecordDefineField 'Parsed ->
-  Sem r (RecordDefineField 'Scoped)
-checkDefineField sig RecordDefineField {..} = do
-  def <- localBindings . ignoreSyntax $ checkFunctionDef _fieldDefineFunDef
-  iden <- checkScopedIden _fieldDefineIden
-  let fname = def ^. signName . nameConcrete
-  unless (HashMap.member fname (sig ^. recordNames)) $
-    throw (ErrUnexpectedField (UnexpectedField fname))
+checkNamedApplicationNew :: forall r. (Members '[Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, NameIdGen] r) => NamedApplicationNew 'Parsed -> Sem r (NamedApplicationNew 'Scoped)
+checkNamedApplicationNew napp = do
+  let nargs = napp ^. namedApplicationNewArguments
+  aname <- checkScopedIden (napp ^. namedApplicationNewName)
+  sig <- if null nargs then return $ NameSignature [] else getNameSignature aname
+  let snames = HashSet.fromList (concatMap (HashMap.keys . (^. nameBlock)) (sig ^. nameSignatureArgs))
+  args' <- withLocalScope . localBindings . ignoreSyntax $ do
+    mapM_ (reserveFunctionSymbol . (^. namedArgumentNewFunDef)) nargs
+    mapM (checkNamedArgumentNew snames) nargs
+  let enames = HashSet.fromList (concatMap (HashMap.keys . (^. nameBlock)) (filter (not . isImplicitOrInstance . (^. nameImplicit)) (sig ^. nameSignatureArgs)))
+      sargs = HashSet.fromList (map (^. namedArgumentNewFunDef . signName . nameConcrete) (toList args'))
+      missingArgs = HashSet.difference enames sargs
+  unless (null missingArgs || not (napp ^. namedApplicationNewExhaustive)) $
+    throw (ErrMissingArgs (MissingArgs (aname ^. scopedIdenFinal . nameConcrete) missingArgs))
  return
-    RecordDefineField
-      { _fieldDefineFunDef = def,
-        _fieldDefineIden = iden
+    NamedApplicationNew
+      { _namedApplicationNewName = aname,
+        _namedApplicationNewArguments = args',
+        _namedApplicationNewAtKw = napp ^. namedApplicationNewAtKw,
+        _namedApplicationNewExhaustive = napp ^. namedApplicationNewExhaustive
+      }
+
+checkNamedArgumentNew ::
+  (Members '[Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, NameIdGen] r) =>
+  HashSet Symbol ->
+  NamedArgumentNew 'Parsed ->
+  Sem r (NamedArgumentNew 'Scoped)
+checkNamedArgumentNew snames NamedArgumentNew {..} = do
+  def <- localBindings . ignoreSyntax $ checkFunctionDef _namedArgumentNewFunDef
+  let fname = def ^. signName . nameConcrete
+  unless (HashSet.member fname snames) $
+    throw (ErrUnexpectedArgument (UnexpectedArgument fname))
+  return
+    NamedArgumentNew
+      { _namedArgumentNewFunDef = def
      }

 checkRecordUpdate :: forall r. (Members '[Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, NameIdGen] r) => RecordUpdate 'Parsed -> Sem r (RecordUpdate 'Scoped)
@ -2257,7 +2242,6 @@ checkNamedApplication ::
  Sem r (NamedApplication 'Scoped)
 checkNamedApplication napp = do
  _namedAppName <- checkScopedIden (napp ^. namedAppName)
-  _namedAppSignature <- Irrelevant <$> getNameSignature _namedAppName
  _namedAppArgs <- mapM checkArgumentBlock (napp ^. namedAppArgs)
  return NamedApplication {..}
  where
@ -2706,10 +2690,10 @@ parseTerm =
      <|> parseLiteral
      <|> parseLet
      <|> parseIterator
-      <|> parseRecordCreation
      <|> parseDoubleBraces
      <|> parseBraces
      <|> parseNamedApplication
+      <|> parseNamedApplicationNew
  where
    parseHole :: Parse Expression
    parseHole = ExpressionHole <$> P.token lit mempty
@ -2791,6 +2775,13 @@ parseTerm =
          AtomNamedApplication u -> Just u
          _ -> Nothing

+    parseNamedApplicationNew :: Parse Expression
+    parseNamedApplicationNew = ExpressionNamedApplicationNew <$> P.token namedApp mempty
+      where
+        namedApp :: ExpressionAtom 'Scoped -> Maybe (NamedApplicationNew 'Scoped)
+        namedApp s = case s of
+          AtomNamedApplicationNew u -> Just u
+          _ -> Nothing
    parseLet :: Parse Expression
    parseLet = ExpressionLet <$> P.token letBlock mempty
      where
@ -2807,14 +2798,6 @@ parseTerm =
          AtomIterator u -> Just u
          _ -> Nothing

-    parseRecordCreation :: Parse Expression
-    parseRecordCreation = ExpressionRecordCreation <$> P.token record mempty
-      where
-        record :: ExpressionAtom 'Scoped -> Maybe (RecordCreation 'Scoped)
-        record s = case s of
-          AtomRecordCreation u -> Just u
-          _ -> Nothing
-
    parseNoInfixIdentifier :: Parse Expression
    parseNoInfixIdentifier = ExpressionIdentifier <$> P.token identifierNoFixity mempty
      where
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
@ -41,11 +41,12 @@ data ScoperError
  | ErrNoNameSignature NoNameSignature
  | ErrNamedArgumentsError NamedArgumentsError
  | ErrNotARecord NotARecord
+  | ErrUnexpectedArgument UnexpectedArgument
  | ErrUnexpectedField UnexpectedField
  | ErrRepeatedField RepeatedField
  | ErrConstructorNotARecord ConstructorNotARecord
  | ErrNotAConstructor NotAConstructor
-  | ErrMissingFields MissingFields
+  | ErrMissingArgs MissingArgs
  | ErrPrecedenceInconsistency PrecedenceInconsistencyError
  | ErrIncomparablePrecedences IncomaprablePrecedences
  | ErrAliasCycle AliasCycle
@ -85,11 +86,12 @@ instance ToGenericError ScoperError where
    ErrNoNameSignature e -> genericError e
    ErrNamedArgumentsError e -> genericError e
    ErrNotARecord e -> genericError e
+    ErrUnexpectedArgument e -> genericError e
    ErrUnexpectedField e -> genericError e
    ErrRepeatedField e -> genericError e
    ErrConstructorNotARecord e -> genericError e
    ErrNotAConstructor e -> genericError e
-    ErrMissingFields e -> genericError e
+    ErrMissingArgs e -> genericError e
    ErrPrecedenceInconsistency e -> genericError e
    ErrIncomparablePrecedences e -> genericError e
    ErrAliasCycle e -> genericError e
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
@ -774,6 +774,27 @@ instance ToGenericError NotARecord where
      i :: Interval
      i = _notARecordLocation

+newtype UnexpectedArgument = UnexpectedArgument
+  { _unexpectedArgument :: Symbol
+  }
+  deriving stock (Show)
+
+instance ToGenericError UnexpectedArgument where
+  genericError UnexpectedArgument {..} = do
+    opts <- fromGenericOptions <$> ask
+    let msg =
+          "Unexpected argument"
+            <+> ppCode opts _unexpectedArgument
+    return
+      GenericError
+        { _genericErrorLoc = i,
+          _genericErrorMessage = mkAnsiText msg,
+          _genericErrorIntervals = [i]
+        }
+    where
+      i :: Interval
+      i = getLoc _unexpectedArgument
+
 newtype UnexpectedField = UnexpectedField
  { _unexpectedField :: Symbol
  }
@ -838,21 +859,21 @@ instance ToGenericError NotAConstructor where
      i :: Interval
      i = getLoc _notAConstructor

-data MissingFields = MissingFields
-  { _missingFieldsConstructor :: Name,
-    _missingFields :: HashSet Symbol
+data MissingArgs = MissingArgs
+  { _missingArgsName :: Name,
+    _missingArgs :: HashSet Symbol
  }
  deriving stock (Show)

-instance ToGenericError MissingFields where
-  genericError MissingFields {..} = do
+instance ToGenericError MissingArgs where
+  genericError MissingArgs {..} = do
    opts <- fromGenericOptions <$> ask
    let msg =
-          "Missing fields for the record constructor"
-            <+> ppCode opts _missingFieldsConstructor
+          "Missing arguments for"
+            <+> ppCode opts _missingArgsName
              <> ":"
              <> line
-              <> itemize (map (ppCode opts) (toList _missingFields))
+              <> itemize (map (ppCode opts) (toList _missingArgs))
    return
      GenericError
        { _genericErrorLoc = i,
@ -861,7 +882,7 @@ instance ToGenericError MissingFields where
        }
    where
      i :: Interval
-      i = getLoc _missingFieldsConstructor
+      i = getLoc _missingArgsName

 newtype PrecedenceInconsistencyError = PrecedenceInconsistencyError
  { _precedenceInconsistencyErrorFixityDef :: FixitySyntaxDef 'Parsed
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@ -684,7 +684,7 @@ expressionAtom =
  P.label "<expression>" $
    AtomLiteral <$> P.try literal
      <|> either AtomIterator AtomNamedApplication <$> iterator
-      <|> AtomRecordCreation <$> recordCreation
+      <|> AtomNamedApplicationNew <$> namedApplicationNew
      <|> AtomNamedApplication <$> namedApplication
      <|> AtomList <$> parseList
      <|> AtomIdentifier <$> name
@ -838,27 +838,26 @@ iterator = do
        _ -> parseFailure off "an iterator must have at least one range"
      return NamedArgument {..}

-recordCreation ::
+namedApplicationNew ::
  forall r.
  (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) =>
-  ParsecS r (RecordCreation 'Parsed)
-recordCreation = P.label "<record creation>" $ do
-  (_recordCreationConstructor, _recordCreationAtKw) <- P.try $ do
+  ParsecS r (NamedApplicationNew 'Parsed)
+namedApplicationNew = P.label "<named application>" $ do
+  (_namedApplicationNewName, _namedApplicationNewAtKw, _namedApplicationNewExhaustive) <- P.try $ do
    n <- name
-    a <- Irrelevant <$> kw kwAt
+    (a, b) <- first Irrelevant <$> ((,False) <$> kw kwAtQuestion <|> (,True) <$> kw kwAt)
    lbrace
-    return (n, a)
+    return (n, a, b)
  defs <- P.sepEndBy (functionDefinition True False Nothing) semicolon
  rbrace
-  let _recordCreationFields = fmap mkField defs
-      _recordCreationExtra = Irrelevant ()
-  return RecordCreation {..}
+  let _namedApplicationNewArguments = fmap mkArg defs
+      _namedApplicationNewExtra = Irrelevant ()
+  return NamedApplicationNew {..}
  where
-    mkField :: FunctionDef 'Parsed -> RecordDefineField 'Parsed
-    mkField f =
-      RecordDefineField
-        { _fieldDefineFunDef = f,
-          _fieldDefineIden = NameUnqualified $ f ^. signName
+    mkArg :: FunctionDef 'Parsed -> NamedArgumentNew 'Parsed
+    mkArg f =
+      NamedArgumentNew
+        { _namedArgumentNewFunDef = f
        }

 namedApplication ::
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@ -11,6 +11,7 @@ module Juvix.Compiler.Internal.Translation.FromConcrete
 where

 import Data.HashMap.Strict qualified as HashMap
+import Data.HashSet qualified as HashSet
 import Data.IntMap.Strict qualified as IntMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Builtins
@ -755,7 +756,7 @@ goExpression = \case
  ExpressionInstanceHole h -> return (Internal.ExpressionInstanceHole h)
  ExpressionIterator i -> goIterator i
  ExpressionNamedApplication i -> goNamedApplication i
-  ExpressionRecordCreation i -> goRecordCreation i
+  ExpressionNamedApplicationNew i -> goNamedApplicationNew i
  ExpressionRecordUpdate i -> goRecordUpdateApp i
  ExpressionParensRecordUpdate i -> Internal.ExpressionLambda <$> goRecordUpdate (i ^. parensRecordUpdate)
  where
@ -764,6 +765,74 @@ goExpression = \case
      s <- ask @NameSignatures
      runReader s (runNamedArguments w) >>= goDesugaredNamedApplication

+    goNamedApplicationNew :: Concrete.NamedApplicationNew 'Scoped -> Sem r Internal.Expression
+    goNamedApplicationNew napp = case nonEmpty (napp ^. namedApplicationNewArguments) of
+      Nothing -> return $ goIden (napp ^. namedApplicationNewName)
+      Just appargs -> do
+        let name = napp ^. namedApplicationNewName . scopedIdenName
+        sig <- fromJust <$> asks @NameSignatures (^. at (name ^. S.nameId))
+        cls <- goArgs appargs
+        let args :: [Internal.Name] = appargs ^.. each . namedArgumentNewFunDef . signName . to goSymbol
+            -- changes the kind from Variable to Function
+            updateKind :: Internal.Subs =
+              HashMap.fromList
+                [ (s, Internal.toExpression s') | s <- args, let s' = Internal.IdenFunction (set Internal.nameKind KNameFunction s)
+                ]
+            napp' =
+              Concrete.NamedApplication
+                { _namedAppName = napp ^. namedApplicationNewName,
+                  _namedAppArgs = nonEmpty' $ createArgumentBlocks (sig ^. nameSignatureArgs)
+                }
+        e <- goNamedApplication napp'
+        let expr =
+              Internal.substitutionE updateKind
+                . Internal.ExpressionLet
+                $ Internal.Let
+                  { _letClauses = cls,
+                    _letExpression = e
+                  }
+        Internal.clone expr
+        where
+          goArgs :: NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
+          goArgs args = nonEmpty' . mkLetClauses <$> mapM goArg args
+            where
+              goArg :: NamedArgumentNew 'Scoped -> Sem r Internal.PreLetStatement
+              goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. namedArgumentNewFunDef)
+
+          createArgumentBlocks :: [NameBlock 'Scoped] -> [ArgumentBlock 'Scoped]
+          createArgumentBlocks sblocks = snd $ foldr goBlock (args0, []) sblocks
+            where
+              args0 :: HashSet S.Symbol = HashSet.fromList $ fmap (^. namedArgumentNewFunDef . signName) (toList appargs)
+              goBlock :: NameBlock 'Scoped -> (HashSet S.Symbol, [ArgumentBlock 'Scoped]) -> (HashSet S.Symbol, [ArgumentBlock 'Scoped])
+              goBlock NameBlock {..} (args, blocks)
+                | null namesInBlock = (args', blocks)
+                | otherwise = (args', block' : blocks)
+                where
+                  namesInBlock =
+                    HashSet.intersection
+                      (HashSet.fromList $ HashMap.keys _nameBlock)
+                      (HashSet.map (^. S.nameConcrete) args)
+                  argNames = HashMap.fromList $ map (\n -> (n ^. S.nameConcrete, n)) $ toList args
+                  args' = HashSet.filter (not . flip HashSet.member namesInBlock . (^. S.nameConcrete)) args
+                  _argBlockArgs = nonEmpty' $ map goArg (toList namesInBlock)
+                  block' =
+                    ArgumentBlock
+                      { _argBlockDelims = Irrelevant Nothing,
+                        _argBlockImplicit = _nameImplicit,
+                        _argBlockArgs
+                      }
+                  goArg :: Symbol -> NamedArgument 'Scoped
+                  goArg sym =
+                    NamedArgument
+                      { _namedArgName = sym,
+                        _namedArgAssignKw = Irrelevant dummyKw,
+                        _namedArgValue = Concrete.ExpressionIdentifier $ ScopedIden name Nothing
+                      }
+                    where
+                      name = over S.nameConcrete NameUnqualified $ fromJust $ HashMap.lookup sym argNames
+                      dummyKw = KeywordRef (asciiKw ":=") dummyLoc Ascii
+                      dummyLoc = getLoc sym
+
    goDesugaredNamedApplication :: DesugaredNamedApplication -> Sem r Internal.Expression
    goDesugaredNamedApplication a = do
      let fun = goScopedIden (a ^. dnamedAppIdentifier)
@ -812,41 +881,6 @@ goExpression = \case
                  let cyc = NonEmpty.reverse ((arg ^. argName) :| c)
                   in throw (ErrDefaultArgCycle (DefaultArgCycle cyc))

-    goRecordCreation :: Concrete.RecordCreation 'Scoped -> Sem r Internal.Expression
-    goRecordCreation Concrete.RecordCreation {..} = do
-      sig :: RecordNameSignature 'Scoped <- fromJust <$> asks @ConstructorNameSignatures (^. at (_recordCreationConstructor ^. Concrete.scopedIdenName . S.nameId))
-      case nonEmpty _recordCreationFields of
-        Nothing -> return (Internal.ExpressionIden (Internal.IdenConstructor (goScopedIden _recordCreationConstructor)))
-        Just (fields1 :: NonEmpty (RecordDefineField 'Scoped)) -> do
-          let getIx fi =
-                let sym = Concrete.symbolParsed (fi ^. Concrete.fieldDefineFunDef . Concrete.signName)
-                 in sig ^?! recordNames . at sym . _Just . nameItemIndex
-              fieldsByIx = nonEmpty' (sortOn getIx (toList fields1))
-          cls <- goFields fieldsByIx
-          let args :: [Internal.Name] = fieldsByIx ^.. each . fieldDefineFunDef . signName . to goSymbol
-              constr = Internal.toExpression (goScopedIden _recordCreationConstructor)
-              e = Internal.foldExplicitApplication constr (map Internal.toExpression args)
-              -- changes the kind from Variable to Function
-              updateKind :: Internal.Subs =
-                HashMap.fromList
-                  [ (s, Internal.toExpression s') | s <- args, let s' = Internal.IdenFunction (set Internal.nameKind KNameFunction s)
-                  ]
-
-          let expr =
-                Internal.substitutionE updateKind
-                  . Internal.ExpressionLet
-                  $ Internal.Let
-                    { _letClauses = cls,
-                      _letExpression = e
-                    }
-          Internal.clone expr
-          where
-            goFields :: NonEmpty (RecordDefineField 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
-            goFields recordfields = nonEmpty' . mkLetClauses <$> mapM goField recordfields
-              where
-                goField :: RecordDefineField 'Scoped -> Sem r Internal.PreLetStatement
-                goField = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. fieldDefineFunDef)
-
    goRecordUpdate :: Concrete.RecordUpdate 'Scoped -> Sem r Internal.Lambda
    goRecordUpdate r = do
      cl <- mkClause
--- a/src/Juvix/Data/Irrelevant.hs
+++ b/src/Juvix/Data/Irrelevant.hs
@ -1,5 +1,3 @@
-- | Used when you annotate some AST with some information that you want to be
-- ignored when checking for equality/ordering
 module Juvix.Data.Irrelevant where

 import Juvix.Data.Loc
@ -7,6 +5,8 @@ import Juvix.Prelude.Base
 import Juvix.Prelude.Pretty
 import Prelude (show)

+-- | Used when you annotate some AST with some information that you want to be
+-- ignored when checking for equality/ordering
 newtype Irrelevant a = Irrelevant
  { _unIrrelevant :: a
  }
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@ -28,6 +28,9 @@ kwExclamation = asciiKw Str.exclamation
 kwAt :: Keyword
 kwAt = asciiKw Str.at_

+kwAtQuestion :: Keyword
+kwAtQuestion = asciiKw Str.atQuestion
+
 kwAxiom :: Keyword
 kwAxiom = asciiKw Str.axiom

--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@ -401,6 +401,9 @@ underscore = "_"
 at_ :: (IsString s) => s
 at_ = "@"

+atQuestion :: (IsString s) => s
+atQuestion = "@?"
+
 dot :: (IsString s) => s
 dot = "."

--- a/test/Compilation/Positive.hs
+++ b/test/Compilation/Positive.hs
@ -412,5 +412,10 @@ tests =
      "Test070: Nested default values and named arguments"
      $(mkRelDir ".")
      $(mkRelFile "test070.juvix")
-      $(mkRelFile "out/test070.out")
+      $(mkRelFile "out/test070.out"),
+    posTest
+      "Test071: Named application"
+      $(mkRelDir ".")
+      $(mkRelFile "test071.juvix")
+      $(mkRelFile "out/test071.out")
  ]
--- a/test/Scope/Negative.hs
+++ b/test/Scope/Negative.hs
@ -293,7 +293,7 @@ scoperErrorTests =
      $(mkRelDir ".")
      $(mkRelFile "NoNamedArguments.juvix")
      $ \case
-        ErrNoNameSignature NoNameSignature {} -> Nothing
+        ErrNamedArgumentsError ErrUnexpectedArguments {} -> Nothing
        _ -> wrongError,
    NegTest
      "Not a record"
@ -321,7 +321,14 @@ scoperErrorTests =
      $(mkRelDir ".")
      $(mkRelFile "MissingFields.juvix")
      $ \case
-        ErrMissingFields {} -> Nothing
+        ErrMissingArgs {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Unexpected argument"
+      $(mkRelDir ".")
+      $(mkRelFile "UnexpectedArgumentNew.juvix")
+      $ \case
+        ErrUnexpectedArgument UnexpectedArgument {} -> Nothing
        _ -> wrongError,
    NegTest
      "Incomparable precedences"
--- a/tests/Compilation/positive/out/test071.out
+++ b/tests/Compilation/positive/out/test071.out
@ -0,0 +1 @@
+1528
--- a/tests/Compilation/positive/test071.juvix
+++ b/tests/Compilation/positive/test071.juvix
@ -0,0 +1,43 @@
+-- Named application
+module test071;
+
+import Stdlib.Data.Nat open hiding {Ord; mkOrd};
+import Stdlib.Data.Nat.Ord as Ord;
+import Stdlib.Data.Product as Ord;
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+
+trait
+type Ord A :=
+  mkOrd {
+    cmp : A -> A -> Ordering;
+    lt : A -> A -> Bool;
+    ge : A -> A -> Bool
+  };
+
+mkOrdHelper
+  {A}
+  (cmp : A -> A -> Ordering)
+  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  : Ord A :=
+  mkOrd cmp lt gt;
+
+instance
+ordNat : Ord Nat := mkOrdHelper@{
+  cmp (x y : Nat) : Ordering := Ord.compare x y
+};
+
+fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1}
+  : Nat := a * b + c;
+
+f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
+
+g {a : Nat := 2} {b : Nat := a + 1} (c : Nat) : Nat := a * b * c;
+
+h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
+
+main : Nat :=
+  fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
+  f@{c := 5} + g@?{b := 4} 3 + if (Ord.lt 1 0) 1 0 +
+  h@?{b := 4} 1;
--- a/tests/negative/UnexpectedArgumentNew.juvix
+++ b/tests/negative/UnexpectedArgumentNew.juvix
@ -0,0 +1,7 @@
+module UnexpectedArgumentNew;
+
+type T := t : T;
+
+f (a : T) : T := t;
+
+x : T := f@{x := t};
--- a/tests/positive/Format.juvix
+++ b/tests/positive/Format.juvix
@ -369,10 +369,10 @@ l3 : List (List Int) :=
 l4 : List (List Int) :=
  [ [1; 2; 3]
  ; longLongLongListArg
-  ; [ longLongLongListArg
-    ; longLongLongListArg
-    ; longLongLongListArg
-    ; longLongLongListArg
+  ; [ longLongLongArg
+    ; longLongLongArg
+    ; longLongLongArg
+    ; longLongLongArg
    ]
  ; longLongLongListArg
  ];