diff --git a/README.md b/README.md index a10b6e2..a6f4b3a 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ To be perfectly clear, `λ` abstractions can be written with either “λ&rd `Π` types can be written with either “Π”, “∀”, or “forall”, and are separated from their bodies with a “,”. Arrow types can be written “->” or “→”. Like with `λ` abstractions, binders with the same type can be grouped, and multiple binders can occur between the “Π” and the “,”. -Finally, `let` expressions have syntax shown below. +`Let` expressions have syntax shown below. let ( ( := ) )+ in end @@ -29,7 +29,15 @@ Below is a more concrete example. and_intro (and A B) C (and_intro A B a b) c end -Definitions work similarly, having abstract syntax as shown below. +You can also directly bind functions. Here’s an example. + + let (f (A : *) (x : A) := x) in + f x + end + +The syntax for binding functions is just like with definitions. + +Definitions have abstract syntax as shown below. ( : )* : ? := | axiom; @@ -172,12 +180,12 @@ Not decidable, but I might be able to implement some basic unification algorithm ### TODO Implicits -Much, much more useful than [inference](#org31a76ab), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. +Much, much more useful than [inference](#orgb7d6c6f), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. ### TODO Module System -A proper module system would be wonderful. To me, ML style modules with structures, signatures, and functors seems like the right way to handle algebraic structures for a relatively simple language, rather than records (or, worse, a bunch of `and`’s like I currently have; especially painful without [implicits](#orge9a1bd4)) or type classes (probably much harder, but could be nicer), but any way of managing scope, importing files, etc. is a necessity. The [F-ing modules](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B573FA00832D55D4878863DE1725D90B/S0956796814000264a.pdf/f-ing-modules.pdf) paper is probably a good reference. +A proper module system would be wonderful. To me, ML style modules with structures, signatures, and functors seems like the right way to handle algebraic structures for a relatively simple language, rather than records (or, worse, a bunch of `and`’s like I currently have; especially painful without [implicits](#orgc3b40df)) or type classes (probably much harder, but could be nicer), but any way of managing scope, importing files, etc. is a necessity. The [F-ing modules](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B573FA00832D55D4878863DE1725D90B/S0956796814000264a.pdf/f-ing-modules.pdf) paper is probably a good reference. ### TODO Universes? diff --git a/README.org b/README.org index b33858e..9dc6d7d 100644 --- a/README.org +++ b/README.org @@ -16,7 +16,7 @@ To be perfectly clear, =λ= abstractions can be written with either "λ" or "fun =Π= types can be written with either "Π", "∀", or "forall", and are separated from their bodies with a ",". Arrow types can be written "->" or "\to". Like with =λ= abstractions, binders with the same type can be grouped, and multiple binders can occur between the "Π" and the ",". -Finally, =let= expressions have syntax shown below. +=Let= expressions have syntax shown below. #+begin_src let ( ( := ) )+ in end #+end_src @@ -30,8 +30,15 @@ Below is a more concrete example. and_intro (and A B) C (and_intro A B a b) c end #+end_src +You can also directly bind functions. Here's an example. +#+begin_src + let (f (A : *) (x : A) := x) in + f x + end +#+end_src +The syntax for binding functions is just like with definitions. -Definitions work similarly, having abstract syntax as shown below. +Definitions have abstract syntax as shown below. #+begin_src ( : )* : ? := | axiom; #+end_src diff --git a/lib/Expr.hs b/lib/Expr.hs index 924751c..376740b 100644 --- a/lib/Expr.hs +++ b/lib/Expr.hs @@ -56,19 +56,25 @@ incIndices = shiftIndices 1 0 parenthesize :: Text -> Text parenthesize s = "(" <> s <> ")" -collectLambdas :: Expr -> ([(Text, Expr)], Expr) +type Param = (Text, Expr) +type ParamGroup = ([Text], Expr) +type Binding = (Text, [ParamGroup], Expr) + +collectLambdas :: Expr -> ([Param], Expr) collectLambdas (Abs x ty body) = ((x, ty) : params, final) where (params, final) = collectLambdas body collectLambdas e = ([], e) -collectLets :: Expr -> ([(Text, Expr)], Expr) -collectLets (Let x val body) = ((x, val) : params, final) +collectLets :: Expr -> ([Binding], Expr) +collectLets (Let x val body) = ((x, params', val') : bindings, final) where - (params, final) = collectLets body + (bindings, final) = collectLets body + (params, val') = collectLambdas val + params' = groupParams params collectLets e = ([], e) -collectPis :: Expr -> ([(Text, Expr)], Expr) +collectPis :: Expr -> ([Param], Expr) collectPis p@(Pi "" _ _) = ([], p) collectPis (Pi x ty body) = ((x, ty) : params, final) where @@ -83,7 +89,7 @@ cleanNames (Pi x ty body) | otherwise = Pi "" ty (cleanNames body) cleanNames e = e -groupParams :: [(Text, Expr)] -> [([Text], Expr)] +groupParams :: [Param] -> [ParamGroup] groupParams = foldr addParam [] where addParam :: (Text, Expr) -> [([Text], Expr)] -> [([Text], Expr)] @@ -92,11 +98,17 @@ groupParams = foldr addParam [] | incIndices t == s = (x : xs, t) : rest | otherwise = ([x], t) : l -showParamGroup :: ([Text], Expr) -> Text +showParamGroup :: ParamGroup -> Text showParamGroup (ids, ty) = parenthesize $ unwords ids <> " : " <> pretty ty -showBinding :: (Text, Expr) -> Text -showBinding (ident, val) = parenthesize $ ident <> " := " <> pretty val +showBinding :: Binding -> Text +showBinding (ident, params, val) = + parenthesize $ + ident + <> " " + <> unwords (map showParamGroup params) + <> " := " + <> pretty val helper :: Integer -> Expr -> Text helper _ (Var s _) = s diff --git a/lib/Parser.hs b/lib/Parser.hs index 31f6fed..62f2b9e 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -104,19 +104,22 @@ pPAbs :: Parser Expr pPAbs = lexeme $ label "Π-abstraction" $ withBinders $ do _ <- defChoice $ "∏" :| ["forall", "∀"] params <- pSomeParams - _ <- defChoice $ pure "," + eat "," body <- pExpr pure $ foldr (uncurry Pi) body params pBinding :: Parser (Text, Expr) pBinding = lexeme $ label "binding" $ do + env <- get eat "(" ident <- pIdentifier + params <- pManyParams eat ":=" value <- pExpr eat ")" + put env modify $ over bindsL (ident :) - pure (ident, value) + pure (ident, foldr (uncurry Abs) value params) pLet :: Parser Expr pLet = lexeme $ label "let expression" $ withBinders $ do