Commit d2893db9 authored by Nicolas Lenz's avatar Nicolas Lenz

Big clean-up

parent e8c2b980
# Katrin
# Lightfold Specification
*Katrin* will be a modern, functional, general-purpose programming language with dependent types.
*Lightfold* will be a modern, functional, general-purpose programming language with dependent types.
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.
At this point it's just [a collection of ideas](ideas.md). You can find the compiler in [its own repo](https://git.eisfunke.com/software/lightfold/compiler).
Ideas, questions, comments, suggestions are always welcome! Feel free to open an issue.
import Katrin.Parse
import qualified Katrin.Core
import qualified Katrin.AST
import System.Environment
import Control.Monad
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 k content where
k = (Katrin.Core.foldExpression Katrin.Core.algebraEval <=< Katrin.Core.foldExpression Katrin.Core.algebraBeta <=< Katrin.Core.foldExpression Katrin.Core.algebraBeta) <$> Katrin.AST.foldKatrin Katrin.AST.algebraKatrinCore <$> katrin
_ -> putStrLn "Invalid argument format"
# Comparisons
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.
This compares some stuff in Haskell wtih how it could look in Lightfold. This is meant to emphasize how Lightfold could cut back on verbosity.
### Simple function with pattern matching
......
# This file contains a wild collection examples of how Katrin code might look.
# This file contains a wild collection examples of how Lightfold code might look.
# No "module" or "package" statement. Only the file name is used.
# Is that a good idea? -> first-class modules
......
bool : type
{True, False}
This diff is collapsed.
name: katrin
version: 0.0.0
license: Apache-2.0
git: "https://git.eisfunke.com/research/katrin"
author: "Nicolas Lenz"
maintainer: "nicolas@eisfunke.com"
copyright: "2018-2019 Nicolas Lenz"
extra-doc-files:
- README.md
synopsis: Experimental functional and dependently-typed programming language
category: Language
description: Please see the README at <https://git.eisfunke.com/research/katrin#readme>
dependencies:
- base
- text
- megaparsec
default-extensions:
- OverloadedStrings
- LambdaCase
library:
source-dirs: src
ghc-options:
- -Wall
- -Wno-name-shadowing
- -Wno-unused-matches
executables:
katrin:
main: main.hs
source-dirs: app
ghc-options:
- -threaded
- -rtsopts
- -with-rtsopts=-N
dependencies:
- katrin
tests:
katrin-test:
main: Main.hs
source-dirs: test
ghc-options:
- -threaded
- -rtsopts
- -with-rtsopts=-N
dependencies:
- katrin
- tasty
- tasty-quickcheck
- quickcheck-instances
# Katrin Roadmap
## 0.1.0
Pure lambda calculus on `int`s
## 0.2.0
Available features:
- Only `int` as data type
- No type annotations as there is no type checking
- Single line comments with `//`
- Definitions
- `int` literals
- Lambdas
- Left-associative prefix function application
- Recursion
- Parentheses
- 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
```
plus
x => 1 => succ x
x => y => plus (succ x) (pred y)
mult
x => 1 => x
x => y => plus x (mult x (pred y))
fac
1 => 1
n => mult n (fac (pred n))
x
5
main
n => fac n
```
module Katrin where
{-# LANGUAGE RecordWildCards#-}
-- | Contains algebras, types and folds for Katrin abstract syntax trees.
module Katrin.AST where
{-
import Data.Text (Text)
import Data.Maybe (fromJust)
import qualified Katrin.Core as Core
{-|
Algebra type (signature) for Katrin AST. This corresponds (is equivalent) to the context-free grammar in ABNF of Katrin:
@
katrin = *definition
definition = identifier "=" expression
expression = 1*segment ; Multiple times for application. Note that 1* means "one or more", not "once"
segment = literal / identifier / identifier "=>" expression / "(" expression ")"
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
}
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 (Text, Core.Expression) Core.Expression Core.Expression
algebraKatrinCore = Algebra {
algebraKatrin = \defs -> fromJust $ lookup "main" defs,
algebraDefinition = \name exp -> (name, exp),
algebraExpression = let
f [] = error "Segments may not be empty"
f (seg:[]) = seg
f (seg:segs) = Core.Application (f segs) seg
in \segs -> f $ reverse segs,
algebraLiteral = \num -> Core.Literal num,
algebraValue = \name -> Core.Value name,
algebraLambda = \name exp -> Core.Lambda name exp,
algebraSubexpression = \exp -> exp
}
-- 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)
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 #-}
-- | Contains algebras, types and folds for KatrinCore, the core language for Katrin.
-- This is currently based on the untyped λ-calculus.
module Katrin.Core where
import Data.Text (Text)
-- Algebra definition
-- | Catamorphic algebraic signature for KatrinCore expressions.
data Algebra expression = Algebra {
algebraBound :: Int -> expression,
algebraFree :: Text -> expression,
algebraApplication :: expression -> expression -> expression,
algebraLambda :: expression -> expression
}
{-
-- | Paramorphic variant of the algebraic signature for KatrinCore.
data AlgebraPara expression = AlgebraPara {
algebraParaValue :: Text -> expression,
algebraParaApplication :: Expression -> expression -> Expression -> expression -> expression,
algebraParaLambda :: Text -> Expression -> expression -> expression
}
-- | Converts an paramorphic algebra to an catamorphic one.
para2cata :: AlgebraPara expression -> Algebra (Expression, expression)
para2cata AlgebraPara{..} = Algebra {
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
= Bound Int
| Free Text
| Application Expression Expression
| Lambda Expression
deriving (Show, Read, Eq)
data Result = Number Int | Function (Int -> Result)
-- Catamorphic fold functions
foldExpression :: Algebra expression -> Expression -> expression
foldExpression alg@Algebra{..} = \case
(Bound index) -> algebraBound index
(Free name) -> algebraFree name
(Application f x) -> algebraApplication (foldExpression alg f) (foldExpression alg x)
(Lambda exp) -> algebraLambda (foldExpression alg exp)
-- Algebras
-- | Term algebra.
algebraTerm :: Algebra Expression
algebraTerm = Algebra Bound Free Application Lambda
data Value
= ValueLambda (Value -> Value)
| ValueNeutral Neutral
data Neutral
= NeutralFree Text
| NeutralApplication Neutral Value
newtype Environment
= Environment [Value]
algebraEval :: Algebra (Environment -> Value)
algebraEval = Algebra {
algebraBound = \index -> \(Environment vals) -> vals !! index,
algebraFree = \name -> \_ -> ValueNeutral (NeutralFree name),
algebraApplication = \f x -> \env -> apply (f env) (x env),
algebraLambda = \exp -> \(Environment vals) -> ValueLambda (\val -> exp (Environment $ val:vals))
}
apply :: Value -> Value -> Value
apply (ValueLambda f) x = f x
apply (ValueNeutral n) x = ValueNeutral (NeutralApplication n x)
-- Helper functions
{-
-- | 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 :: 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 algebras, types and folds for KatrinLite, the desugared version of Katrin.
module Katrin.Lite where
-- | Contains the parser for Katrin.
module Katrin.Parse where
import Katrin.AST
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
-- | Main parser typedef. Parsing is done on Text without custom error component.
type Parser = Parsec Void Text
-- Lexer
-- | Comment parsers.
lineComment, blockComment :: Parser ()
lineComment = L.skipLineComment "//"
blockComment = L.skipBlockCommentNested "/*" "*/"
-- | Space consumer
sc :: Parser ()
sc = skipSome $ choice [skipSome $ char ' ', lineComment, blockComment]
-- | Space consumer including newlines, for between defintions
scn :: Parser ()
scn = L.space (skipSome $ char ' ' <|> char '\n') lineComment blockComment
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) <?> "literal"
identifier :: Parser Text
identifier = (lexeme . try) (T.pack <$> ((:) <$> letterChar <*> many alphaNumChar)) <?> "identifier"
-- Parser
katrin :: Parser Katrin
katrin = between scn eof (Katrin <$> definition `sepEndBy1` scn)
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)
<|> try (Value <$> identifier)
<|> try (Subexpression <$> parens expression <?> "parenthized subexpression")
resolver: lts-14.6
# This file was autogenerated by Stack.
# You should not edit this file by hand.
# For more information, please see the documentation at:
# https://docs.haskellstack.org/en/stable/lock_files
packages: []
snapshots:
- completed:
size: 524127
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/6.yaml
sha256: dc70dfb45e2c32f54719819bd055f46855dd4b3bd2e58b9f3f38729a2d553fbb
original: lts-14.6
main = ( x => y => (succ (succ y)) ) 3 4
\ No newline at end of file
module Main where
import Test.Tasty
import Test.Tasty.QuickCheck
import Test.QuickCheck.Instances
import Katrin.Core
import Katrin.Algebra
import Data.Text
main :: IO ()
main = defaultMain test
test :: TestTree
test = testGroup "Main tests" [
testProperty "Identity of folding in Katrin term algebra" prop_foldTermKatrinIdentic]
prop_foldTermKatrinIdentic :: Katrin -> Bool
prop_foldTermKatrinIdentic k = foldKatrin katrinAlgTerm k == k
instance Arbitrary Katrin where
arbitrary = sized $ \n -> Katrin <$> resize (n`div`2) arbitrary <*> resize (n`div`2) arbitrary
instance Arbitrary Identifier where
arbitrary = Identifier <$> resize 5 arbitrary
instance Arbitrary Pattern where
arbitrary = undefined
instance Arbitrary Expression where
arbitrary = sized $ \n ->
frequency [
(1, Literal <$> arbitrary),
(n, Application <$> resize (n`div`2) arbitrary <*> resize (n`div`2) arbitrary),
(n, Lambda <$> resize (n`div`2) arbitrary <*> resize (n`div`2) arbitrary)]
instance Arbitrary Definition where
arbitrary = sized $ \n ->
Definition <$> arbitrary <*> resize (n`div`2) arbitrary <*> resize (n`div`2) arbitrary
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