Commit 1543533d authored by Nicolas Lenz's avatar Nicolas Lenz

Great stuff happening. First Katrin types, algebras and catamorphisms are done.

parent b4b4b26e
......@@ -18,7 +18,7 @@ Please be aware that at this point this document is just a collection of quite r
### Interaction-oriented
Interaction (with users, windows, servers, ...) is a very important thing in programming. Unfortunately, it is quite awkward (especially for beginners) in many functional languages. Find better solutions.
Interaction (with users, windows, servers, ...) is a very important thing in programming. Unfortunately, it is quite awkward (especially for beginners) in many functional languages. Find better solutions working without loads of monad transformers.
Good GUI solutions are important. Haskell still has no reasonable GUI solutions, which is really hindering adoption. Interaction-oriented language design could help.
......@@ -33,11 +33,8 @@ Good GUI solutions are important. Haskell still has no reasonable GUI solutions,
### Data-centric
- Communication with databases/files/servers/users should easy and type-safe
- ~~If possible: simultaneously markup-/data-language?~~
- Bad idea. Better stick to YAML as encouraged default. It can represent record types very well and is already established and less awkward to write.
- Deriving of serialization traits should be generically possible.
- Integration with CrystalOS file/return type system, one day
- Communication with databases/files/servers/users should easy and type-safe.
- Implicit typed reading of files (integration with typed file system of CrystalOS)
- ~~*Languages* (regular, context-free) at the language heart~~
- Probably nonsense
......
{-# LANGUAGE OverloadedStrings #-}
module Katrin where
-- well.
import Prelude hiding (String) -- so I don't accidentally use String instead of Text
import Data.Text (Text)
import qualified Data.Text as Text
-- List stuff just for trying out algebras, nothing to do with Katrin
data List a = Nil | Cons {hd :: a, tl :: List a}
data ListAlg a target = ListAlg {
algNil :: target,
algCons :: a -> target -> target
}
-- 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)
foldListExample :: Int
foldListExample = foldList (ListAlg 0 (+)) (Cons 1 $ Cons 2 $ Cons 42 Nil) -- = 1 + 2 + 42 = 45
-- | Main data type for a Katrin library consisting of a list of type definitions and a list of definitions.
data Katrin = Katrin {typeDefs :: [TypeDef], defs :: [Def]} deriving (Show, Read, Eq)
-- | Type for an identifier of a value, like an integer, a function, a type etc.
newtype ValueId = ValueId Text deriving (Show, Read, Eq)
-- | Type for an identifier of a constructor.
newtype ConstrId = ConstrId Text deriving (Show, Read, Eq)
-- | A type definition, consisting of an identifier for the type and the corresponding type expression.
data TypeDef = TypeDef {
typeId :: ValueId,
typeExp :: TypeExp
} deriving (Show, Read, Eq)
-- | A type expression, consisting of stuff.
-- TODO explain that. I'm too lazy right now.
data TypeExp = ProductType ConstrId [ValueId] | SumType TypeExp TypeExp
deriving (Show, Read, Eq)
data Def = Def {
expId :: ValueId,
expType :: Exp,
exp :: Exp
} deriving (Show, Read, Eq)
data Exp =
Literal ConstrId
| Application {function :: Exp, argument :: Exp}
| Variable {symbol :: ValueId}
| Lambda {inPattern :: Exp, outExp :: Exp}
deriving (Show, Read, Eq)
-- | Algebra / grammar for Katrin.
data KatrinAlg katrin valueId constrId typeDef def typeExp exp = KatrinAlg {
katrinAlg :: [typeDef] -> [def] -> katrin,
valueIdAlg :: Text -> valueId,
constrIdAlg :: Text -> constrId,
typeDefAlg :: valueId -> typeExp -> typeDef,
productTypeAlg :: constrId -> [valueId] -> typeExp,
sumTypeAlg :: typeExp -> typeExp -> typeExp,
defAlg :: valueId -> exp -> exp -> def,
literalAlg :: constrId -> exp,
applicationAlg :: exp -> exp -> exp,
variableAlg :: valueId -> exp,
lambdaAlg :: exp -> exp -> exp
}
-- Catamorphic fold functions for Katrin.
foldKatrin :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Katrin -> katrin
foldKatrin alg (Katrin tds ds) = katrinAlg alg (foldTypeDef alg <$> tds) (foldDef alg <$> ds)
foldValueId :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> ValueId -> valueId
foldValueId alg (ValueId t) = valueIdAlg alg t
foldConstrId :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> ConstrId -> constrId
foldConstrId alg (ConstrId t) = constrIdAlg alg t
foldTypeDef :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> TypeDef -> typeDef
foldTypeDef alg (TypeDef vid te) = typeDefAlg alg (foldValueId alg vid) (foldTypeExp alg te)
foldTypeExp :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> TypeExp -> typeExp
foldTypeExp alg (ProductType cid vids) = productTypeAlg alg (foldConstrId alg cid) (foldValueId alg <$> vids)
foldTypeExp alg (SumType te1 te2) = sumTypeAlg alg (foldTypeExp alg te1) (foldTypeExp alg te2)
foldDef :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Def -> def
foldDef alg (Def vid e1 e2) = defAlg alg (foldValueId alg vid) (foldExp alg e1) (foldExp alg e2)
foldExp :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Exp -> exp
foldExp alg (Literal cid) = literalAlg alg (foldConstrId alg cid)
foldExp alg (Application e1 e2) = applicationAlg alg (foldExp alg e1) (foldExp alg e2)
foldExp alg (Variable vid) = variableAlg alg (foldValueId alg vid)
foldExp alg (Lambda e1 e2) = lambdaAlg alg (foldExp alg e1) (foldExp alg e2)
-- | 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 :: KatrinAlg Katrin ValueId ConstrId TypeDef Def TypeExp Exp
katrinAlgTerm = KatrinAlg {
katrinAlg = Katrin, valueIdAlg = ValueId, constrIdAlg = ConstrId,
typeDefAlg = TypeDef, productTypeAlg = ProductType, sumTypeAlg = SumType,
defAlg = Def, literalAlg = Literal, applicationAlg = Application,
variableAlg = Variable, lambdaAlg = Lambda
}
-- | An example type definition for natural numbers.
-- Corresponds to "data Nat = One | Succ Nat".
typeExampleNat :: TypeDef
typeExampleNat = TypeDef
(ValueId "Nat")
$ SumType (ProductType (ConstrId "One") []) (ProductType (ConstrId "Succ") [ValueId "Nat"])
defExampleNat :: Def
defExampleNat = Def
(ValueId "two")
(Variable $ ValueId "Nat")
(Application (Variable $ ValueId "Succ") (Variable $ ValueId "One"))
katrinExample01 :: Katrin
katrinExample01 = Katrin
[typeExampleNat] -- type defs
[defExampleNat] -- defs
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