Commit 8e59b6ac authored by Nicolas Lenz's avatar Nicolas Lenz

A whole lot of stuff.

- Built a primitve parser
- Built a AST type and folds
- Some refactoring and moving stuff around
parent c696b850
......@@ -2,6 +2,6 @@
*Katrin* is a modern, functional, general-purpose programming language with dependent types.
At this point it's just [a wild collection of ideas](ideas.md) and [some examples of future code](example.katrin) and some ground work for an algebraic compiler written in Haskell.
At this point it's just [a collection of ideas](ideas.md), [some examples of future code](example.katrin) and some ground work for an algebraic compiler written in Haskell.
Ideas, comments and suggestions are always welcome!
module Main where
import Katrin
import Katrin.Core
import Katrin.Algebra
import System.Environment
-- | An excellent main function.
main :: IO ()
main = do
args <- getArgs
let n = read (head args) :: Int
let exp = Application ( (Lambda "x") (Application (Value "succ") (Value "x")) ) (Literal n)
print $ (foldExpression algKatrinEval =<< foldExpression algKatrinBeta =<< foldExpression algKatrinBeta exp)
import Katrin.Parse
import System.Environment
import Data.Text.IO as T (readFile)
import Text.Megaparsec
-- | An excellent main function.
main :: IO ()
main = getArgs >>= \case
[file] -> do
content <- T.readFile file
parseTest katrin content
_ -> putStrLn "Invalid argument format"
# Comparisons
This compares some stuff in Haskell wtih how it could look in Katrin.
This compares some stuff in Haskell wtih how it could look in Katrin. This is meant to emphasize how Katrin could cut back on verbosity.
### Simple function with pattern matching
......
......@@ -2,6 +2,8 @@
Please be aware that at this point this document is just a collection of quite random notes and ideas.
TODO: Clean this up
## Features
### Functional
......
......@@ -6,7 +6,7 @@ author: "Nicolas Lenz"
maintainer: "nicolas@eisfunke.com"
copyright: "2018-2019 Nicolas Lenz"
extra-source-files:
extra-doc-files:
- README.md
synopsis: Experimental functional and dependently-typed programming language
......@@ -16,6 +16,7 @@ description: Please see the README at <https://git.eisfunke.com/research
dependencies:
- base
- text
- megaparsec
default-extensions:
- OverloadedStrings
......@@ -30,7 +31,7 @@ library:
executables:
katrin:
main: Main.hs
main: main.hs
source-dirs: app
ghc-options:
- -threaded
......
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards#-}
-- | Contains algebras, types and folds for Katrin abstract syntax trees.
module Katrin where
import Katrin.Core
import Data.Text (Text)
import qualified Katrin.Core as Core
import Prelude hiding (String) -- so I don't accidentally use String instead of Text
{-|
Algebra for Katrin AST. This corresponds (is equivalent) to the context-free grammar in ABNF of Katrin:
-- List stuff just for trying out algebras, nothing to do with Katrin
@
katrin = *definition
definition = identifier "=" expression
data List a = Nil | Cons {hd :: a, tl :: List a}
expression = 1*segment ; Multiple times for application. Note that 1* means "one or more", not "once"
segment = literal / identifier / identifier "=>" expression / "(" expression ")"
data ListAlg a target = ListAlg {
algNil :: target,
algCons :: a -> target -> target
literal = ["-" / "+"] 1*DIGIT
identifier = ALPHA *(ALPHA / DIGIT)
@
-}
data Algebra katrin definition expression segment = Algebra {
algebraKatrin :: [definition] -> katrin,
algebraDefinition :: Text -> expression -> definition,
algebraExpression :: [segment] -> expression,
algebraLiteral :: Int -> segment,
algebraValue :: Text -> segment,
algebraLambda :: Text -> expression -> segment,
algebraSubexpression :: expression -> segment
}
-- Note that this is equivalent to a normal foldr
foldList :: ListAlg a target -> List a -> target
foldList alg Nil = algNil alg
foldList alg (Cons x xs) = algCons alg x (foldList alg xs)
newtype Katrin = Katrin [Definition]
deriving (Show)
data Definition = Definition Text Expression
deriving (Show)
newtype Expression = Expression [Segment]
deriving (Show)
data Segment = Literal Int | Value Text | Lambda Text Expression | Subexpression Expression
deriving (Show)
-- Algebras
algebraTerm :: Algebra Katrin Definition Expression Segment
algebraTerm = Algebra Katrin Definition Expression Literal Value Lambda Subexpression
algebraKatrinCore :: Algebra Core.Expression b c d
algebraKatrinCore = undefined -- TODO
-- Catamorphic fold functions
foldKatrin :: Algebra katrin definition expression segment -> Katrin -> katrin
foldKatrin alg@Algebra{..} (Katrin defs) = algebraKatrin (foldDefinition alg <$> defs)
foldDefinition :: Algebra katrin def exp seg -> Definition -> def
foldDefinition alg@Algebra{..} (Definition name exp) = algebraDefinition name (foldExpression alg exp)
foldExpression :: Algebra katrin definition expression segment -> Expression -> expression
foldExpression alg@Algebra{..} (Expression segs) = algebraExpression (foldSegment alg <$> segs)
foldListExample :: Int
foldListExample = foldList (ListAlg 0 (+)) (Cons 1 $ Cons 2 $ Cons 42 Nil) -- = 1 + 2 + 42 = 45
foldSegment :: Algebra katrin definition expression segment -> Segment -> segment
foldSegment alg@Algebra{..} = \case
Literal num -> algebraLiteral num
Value txt -> algebraValue txt
Lambda txt exp -> algebraLambda txt (foldExpression alg exp)
Subexpression exp -> algebraSubexpression (foldExpression alg exp)
{-# LANGUAGE RecordWildCards #-}
module Katrin.Algebra where
import Katrin.Core
import Data.Text (Text)
-- | Algebraic signature (which is the context-free grammar for the tokens) for Katrin.
data AlgKatrin expression = AlgKatrin {
algLiteral :: Int -> expression,
algValue :: Text -> expression,
algApplication :: expression -> expression -> expression,
algLambda :: Text -> expression -> expression
}
{-
-- | Paramorphic variant of the algebraic signature for Katrin.
data AlgParaKatrin katrin definition identifier expression pattern = AlgParaKatrin {
algParaKatrin :: [Definition] -> [definition] -> katrin,
algParaDefinition :: Identifier -> identifier -> Expression -> expression -> definition,
algParaIdentifier :: Text -> identifier,
algParaLiteral :: Int -> expression,
algParaValue :: Identifier -> identifier -> expression,
algParaApplication :: Expression -> expression -> Expression -> expression -> expression,
algParaLambda :: Pattern -> pattern -> Expression -> expression -> expression,
algParaBind :: Identifier -> identifier -> pattern,
algParaMatch :: Int -> pattern
}
para2cata_katrin ::
AlgParaKatrin katrin definition identifier expression pattern
-> AlgKatrin (Katrin, katrin) (Definition, definition) (Identifier, identifier) (Expression, expression) (Pattern, pattern)
para2cata_katrin AlgParaKatrin{..} = AlgKatrin {
algKatrin = \defs' -> let (defPs, defs) = unzip defs' in (Katrin defPs, algParaKatrin defPs defs),
algDefinition = \(idP, id) (expP, exp) -> (Definition idP expP, algParaDefinition idP id expP exp),
algIdentifier = \text -> (Identifier text, algParaIdentifier text),
algLiteral = \num -> (Literal num, algParaLiteral num),
algValue = \(idP, id) -> (Value idP, algParaValue idP id),
algApplication = \(exp1P, exp1) (exp2P, exp2) -> (Application exp1P exp2P, algParaApplication exp1P exp1 exp2P exp2),
algLambda = \(patP, pat) (expP, exp) -> (Lambda patP expP, algParaLambda patP pat expP exp),
algBind = \(idP, id) -> (Bind idP, algParaBind idP id),
algMatch = \num -> (Match num, algParaMatch num)
}
-}
-- Catamorphic fold functions
{-
foldKatrin :: AlgKatrin katrin expression -> Katrin -> katrin
foldKatrin alg (Katrin exp) = algKatrin alg (foldExpression alg exp)
-}
foldExpression :: AlgKatrin expression -> Expression -> expression
foldExpression alg = \case
(Literal num) -> algLiteral alg num
(Value txt) -> algValue alg txt
(Application exp1 exp2) -> algApplication alg (foldExpression alg exp1) (foldExpression alg exp2)
(Lambda txt exp) -> algLambda alg txt (foldExpression alg exp)
-- Algebras
-- | Term algebra for Katrin. `foldKatrin katrinAlgTerm` folds a Katrin term into a, well, Katrin term.
-- Useful for compilation into a Katrin term and for testing.
katrinAlgTerm :: AlgKatrin Expression
katrinAlgTerm = AlgKatrin Literal Value Application Lambda
-- | Algebra that performs β-reduction on Katrin.
algKatrinBeta :: AlgKatrin (Either Text Expression)
algKatrinBeta = AlgKatrin {
algLiteral = Right . Literal,
algValue = Right . Value,
algApplication = \exp1' exp2' -> do
exp1 <- exp1'
exp2 <- exp2'
case exp1 of
Lambda txt exp -> Right $ bind txt exp2 exp
Value "succ" -> case exp2 of
Literal n -> Right $ Literal $ n+1
_ -> Right $ Application exp1 exp2
Value txt -> Right $ Application exp1 exp2
_ -> Left "Trying to apply something to a non-function.",
algLambda = \txt exp -> exp >>= (Right . Lambda txt)
}
algKatrinEval :: AlgKatrin (Either Text Int)
algKatrinEval = AlgKatrin {
algLiteral = \num -> Right num,
algValue = \txt -> Left $ "Unresolved identifier " <> txt,
algApplication = \exp1' exp2' -> Left "Unapplied Application",
algLambda = \txt exp -> Left "Unapplied Lambda"
}
-- | Replaces all values in an expression with fitting identifier with literal values
bind :: Text -- Identifier to bind
-> Expression -- Expression to paste
-> Expression -- Expression to bind in
-> Expression -- Result
bind bindId arg = \case
Literal num -> Literal num
Value id
| id == bindId -> arg
| otherwise -> Value id
Application exp1 exp2 -> Application (bind bindId arg exp1) (bind bindId arg exp2)
Lambda txt exp
| txt == bindId -> Lambda txt exp
| otherwise -> Lambda txt (bind bindId arg exp)
{-
algKatrinTemplate :: AlgKatrin katrin identitfier pattern expression definition
algKatrinTemplate = AlgKatrin {
algKatrin = \defs -> undefined,
algIdentifier = \txt -> undefined,
algBind = \id -> undefined,
algMatch = \num -> undefined,
algLiteral = \num -> undefined,
algValue = \id -> undefined,
algApplication = \exp1 exp2 -> undefined,
algLambda = \pat exp -> undefined,
algDefinition = \id exp -> undefined
}
-}
{-# LANGUAGE RecordWildCards #-}
-- | Contains algebras, types and folds for KatrinCore, the intermediate language for Katrin.
module Katrin.Core where
import Data.Text (Text)
-- | Main data type for a Katrin library consisting of a list of type definitions and a list of definitions.
newtype Katrin = Katrin Expression
deriving (Show, Read, Eq)
-- Algebra definition
-- | Catamorphic algebraic signature for KatrinCore expressions.
data Algebra expression = Algebra {
algebraLiteral :: Int -> expression,
algebraValue :: Text -> expression,
algebraApplication :: expression -> expression -> expression,
algebraLambda :: Text -> expression -> expression
}
-- | Paramorphic variant of the algebraic signature for KatrinCore.
data AlgebraPara expression = AlgebraPara {
algebraParaLiteral :: Int -> expression,
algebraParaValue :: Text -> expression,
algebraParaApplication :: Expression -> expression -> Expression -> expression -> expression,
algebraParaLambda :: Text -> Expression -> expression -> expression
}
-- | Type for expressions, which are either a literal, a value identifier, a function application or a lambda function.
-- | Converts an paramorphic algebra to an catamorphic one.
para2cata :: AlgebraPara expression -> Algebra (Expression, expression)
para2cata AlgebraPara{..} = Algebra {
algebraLiteral = \num -> (Literal num, algebraParaLiteral num),
algebraValue = \txt -> (Value txt, algebraParaValue txt),
algebraApplication = \(exp1P, exp1) (exp2P, exp2) -> (Application exp1P exp2P, algebraParaApplication exp1P exp1 exp2P exp2),
algebraLambda = \txt (expP, exp) -> (Lambda txt expP, algebraParaLambda txt expP exp)
}
-- Type definition
-- | Type for lambda expressions, which are either a literal, a value identifier, a function application or a lambda function.
data Expression =
Literal Int
| Value Text
......@@ -16,55 +44,84 @@ data Expression =
data Result = Number Int | Function (Int -> Result)
{-
instance Show Result where
show (Number num) = "Number " <> show num
show (Function f) = "[Function]"
-- Catamorphic fold functions
instance Monoid a => Alternative (Either a) where
empty = Left mempty
(<|>) = mplus
foldExpression :: Algebra expression -> Expression -> expression
foldExpression alg@Algebra{..} = \case
(Literal num) -> algebraLiteral num
(Value txt) -> algebraValue txt
(Application exp1 exp2) -> algebraApplication (foldExpression alg exp1) (foldExpression alg exp2)
(Lambda txt exp) -> algebraLambda txt (foldExpression alg exp)
instance Monoid a => MonadPlus (Either a) where
mzero = Left mempty
mplus (Right x) _ = Right x
mplus _ y = y
-- Algebras
-- | Term algebra.
algebraTerm :: Algebra Expression
algebraTerm = Algebra Literal Value Application Lambda
lookupDefinition :: [Definition] -> Identifier -> Either Text [Expression]
lookupDefinition [] _ = Left "Reached end while looking up definitions"
lookupDefinition (Definition defId exps:defs) id
| defId == id = Right exps
| otherwise = lookupDefinition defs id
asValue :: [Expression] -> Either Text Int
asValue (Literal num:exps) = Right num
asValue x = Left $ "Trying to use a non-literal as value: " <> pack (show x)
asFunction :: [Expression] -> Int -> [Expression]
asFunction (Lambda pat exp : exps) arg = case pat of
Bind id -> bind id arg exp : asFunction exps arg
Match num
| num == arg -> exp : asFunction exps arg
| otherwise -> exps
asFunction (_:exps) arg = asFunction exps arg
asFunction [] _ = []
-- | Algebra that performs β-reduction on Katrin.
algebraBeta :: Algebra (Either Text Expression)
algebraBeta = Algebra {
algebraLiteral = Right . Literal,
algebraValue = Right . Value,
algebraApplication = \exp1' exp2' -> do
exp1 <- exp1'
exp2 <- exp2'
case exp1 of
Lambda txt exp -> Right $ bind txt exp2 exp
Value "succ" -> case exp2 of
Literal n -> Right $ Literal $ n+1
_ -> Right $ Application exp1 exp2
Value txt -> Right $ Application exp1 exp2
_ -> Left "Trying to apply something to a non-function.",
algebraLambda = \txt exp -> exp >>= (Right . Lambda txt)
}
-- | Algebra for evaluating an β-reduced expression.
algebraEval :: Algebra (Either Text Int)
algebraEval = Algebra {
algebraLiteral = \num -> Right num,
algebraValue = \txt -> Left $ "Unresolved identifier " <> txt,
algebraApplication = \exp1' exp2' -> Left "Unapplied Application",
algebraLambda = \txt exp -> Left "Unapplied Lambda"
}
-- Helper functions
-- | Replaces all values in an expression with fitting identifier with literal values
bind :: Identifier -> Int -> Expression -> Expression
bind :: Text -- ^ Identifier to bind
-> Expression -- ^ Expression to paste
-> Expression -- ^ Expression to bind in
-> Expression -- ^ Result
bind bindId arg = \case
Literal num -> Literal num
Value id
| id == bindId -> Literal arg
| id == bindId -> arg
| otherwise -> Value id
Application exp1 exp2 -> Application (bind bindId arg exp1) (bind bindId arg exp2)
Lambda pat exp -> case pat of
Bind id
| id == bindId -> Lambda pat exp
| otherwise -> Lambda pat (bind bindId arg exp)
Match num -> Lambda pat (bind bindId arg exp)
Lambda txt exp
| txt == bindId -> Lambda txt exp
| otherwise -> Lambda txt (bind bindId arg exp)
{-
apply :: Expression -> Expression -> Either Text Expression
apply exp1 exp2 = case exp1 of
Value (Identifier "succ") -> asValue [exp2] >>= return . Literal . (+1)
algKatrinTemplate :: AlgKatrinCore katrin identitfier pattern expression definition
algKatrinTemplate = AlgKatrinCore {
algLiteral = \num -> undefined,
algValue = \txt -> undefined,
algApplication = \exp1 exp2 -> undefined,
algLambda = \txt exp -> undefined
}
-}
{-
instance Monoid a => Alternative (Either a) where
empty = Left mempty
(<|>) = mplus
instance Monoid a => MonadPlus (Either a) where
mzero = Left mempty
mplus (Right x) _ = Right x
mplus _ y = y
-}
-- | Contains the parser for Katrin.
module Katrin.Parse where
import Katrin
import Data.Text (Text)
import qualified Data.Text as T
import Data.Void
import Text.Megaparsec
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
type Parser = Parsec Void Text
-- Lexer
sc :: Parser ()
sc = L.space space1 lineComment blockComment where
lineComment = L.skipLineComment "//"
blockComment = L.skipBlockCommentNested "/*" "*/"
lexeme :: Parser a -> Parser a
lexeme = L.lexeme sc
symbol :: Text -> Parser ()
symbol = (>> return ()) . L.symbol sc
parens :: Parser a -> Parser a
parens = between (symbol "(") (symbol ")")
literal :: Parser Int
literal = lexeme $ L.signed sc L.decimal
identifier :: Parser Text
identifier = (lexeme . try) (T.pack <$> ((:) <$> letterChar <*> many alphaNumChar))
-- Parser
-- TODO: Newlines/multiple definitions don't work, they are taken as parts of the previous definition
katrin :: Parser Katrin
katrin = between sc eof (Katrin <$> many definition)
definition :: Parser Definition
definition = Definition <$> identifier <* symbol "=" <*> expression
expression :: Parser Expression
expression = Expression <$> some segment
segment :: Parser Segment
segment =
try (Lambda <$> identifier <* symbol "=>" <*> expression <?> "lambda expression")
<|> try ((Literal <$> literal) <?> "literal")
<|> try (Value <$> identifier <?> "identifier")
<|> try (Subexpression <$> parens expression <?> "subexpression")
......@@ -8,17 +8,17 @@ Pure lambda calculus on `int`s
Available features:
- Only `nat` as data type
- Only `int` as data type
- No type annotations as there is no type checking
- Single line comments with `//`
- Definitions
- `nat` literals
- `int` literals
- Lambdas
- Left-associative prefix function application
- Recursion
- Parentheses
- Predefined functions: `succ : nat -> nat`, `pred : nat -> nat` (partial)
- `main : nat -> nat`
- Predefined functions: `succ : int -> int`, `pred : int -> int` (partial)
- `main : int -> int`
- Compiled program takes one parameter with the argument and prints the result out
```
......
main = kek => ( succ 3 )
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment