The vague idea of a modern dependently-typed programming language.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

#### example.katrin 4.8KB Permalink History Raw

 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240 # This file contains a wild collection examples of how Katrin code might look. # No "module" or "package" specification. Only the file name is used. # I might be clinging to Haskell syntax too much. I might need to get more independent. # No weird split between paackage name and module names like Haskell does or 1000 char long names like in Java import "packageName.module" Type = Set Universe // The backend of this needs a lot of thought. // Maybe some category theory could do... something. Nat : Type One : Nat Succ : Nat -> Nat Nat0 : Type Zero : Nat0 Succ : Nat0 -> Nat0 Maybe : Type -> Type Nothing : Maybe a Just : a -> Maybe a Pair : Type -> Type -> Type Pair : a -> b -> Pair a b List : Type -> Type Empty : List t Cons : t -> List t -> List t Vector : Nat -> Type -> Type Single : t -> Vector One t Cons : t -> Vector n t -> Vector (Succ n) t a : Vector 2 Nat Single One # Type mismatch for a! Expected Vector 2 Nat, got Vector 1 Nat b : Vector 3 Nat 1 2 Single 3 c : Vector 3 Nat [1,2,3] # Lists are overloaded # b == c PersonT : Type MkPerson : String -> Int -> Person personT : PersonT MkPerson "Peter" 25 PersonC : Type Name : Person -> String Age: Person -> Int personC : personC Name = "Peter" Age = 25 CoList : Type -> Type Split : CoList a -> Maybe (a, CoList a) isOne : Nat -> Bool One => True _ => False plus' : Nat -> Nat -> Nat One => y => Succ y Succ x => y => plus' x (Succ y) syntax infix plus as + /* isOne :: Nat -> Bool isOne One = True isOne _ = False */ main : Actor = new Actor input = String Integer : Type Zero : Integer Plus : Nat -> Integer Minus : Nat -> Integer CoNat : CoType Pred : CoNat -> Maybe CoNat Three : Nat = Succ (Succ One) CoTwo : CoNat = {Pred = Just {Pred = Nothing}} # Provisional record syntax borrowed from Haskell, I'll need to think of something better. coPlus : CoNat -> CoNat -> CoNat x => y => case Pred y Just y' -> {Pred = Just x} coPlus y' ls = map (x => x *3) [1,2,3] # [3,6,9] [Set|1,2,3] == [Set|3,2,1] # Lambda syntax: in1 => in2 => out # Function definition uses normal lambda syntax # Pros: One syntax rule less, less parentheses needed as the => are clear separators f : Nat -> Nat x => x + 10 OneTwoThree : List Int OneTwoThree = Cons 1 (Cons 2 (Cons 3 Empty)) CoOneTwoThree : CoList Int CoOneTwoThree = Just (1, Just (2, (Just 3, Nothing))) Nat : Type Nat = Nat Pair _ _ : Set -> Set -> Set Pair a b = type Pair : (first : a) -> (second : b) -> Pair a b # Rethink this together with the Set/Type stuff Person : Set Person = {Alice, Bob} bestPair : Pair Person Person bestPair = Pair Alice Bob test : Set test = {Kek, Lel, Topkek} # Traits for algebraic structures for calculating. trait Magma a * : a -> a -> a trait (Magma a) ⇒ Semigroup a (x * y) * z == x * (y * z) trait (Semigroup a) ⇒ Monoid a 1 : a 1 * x == x x * 1 == x trait (Monoid a) ⇒ Group a 1/ _ : a -> a trait (Group a) ⇒ AbelianGroup a x * y == y * x # Define all those analogously, but named "Co" and with + instead of *. # Is there a more elegant way? Named instances or something? trait CoMagma a _ + _ : a -> a -> a trait (CoMagma a) ⇒ CoSemigroup a (x + y) + z == x + (y + z) trait (CoSemigroup a) ⇒ CoMonoid a 0 : a 0 + x == x x + 0 == x trait (CoMonoid a) ⇒ CoAbelianMonoid a x + y == y + x trait (CoMonoid a) ⇒ CoGroup a - _ : a -> a trait (CoGroup a, CoAbelianMonoid a) ⇒ CoAbelianGroup a trait (Monoid a, CoAbelianMonoid a) ⇒ Semiring a x * (y + z) = (x * y) + (x * z) (y + z) * x = (y * x) + (z * x) trait (Semiring a, CoAbelianGroup a) ⇒ Ring a trait (Ring a, AbelianGroup a/0) ⇒ Field a # Probably using less mathematical and more concrete names would be a good idea. # Instances for Nat and Integer. This should make normale calculations using those types possible. instance CoMagma Nat x + Zero = x x + (Succ y) = (Succ x) + y instance CoMagma Integer x + Zero = x Zero + y = y Plus x + Plus y = x + y Minus x + Minus y = Minus (x + y) Plus (Succ x) + Minus One = Plus x Plus (Succ x) + Minus (Succ y) = Plus x + Minus y Plus One + Minus (Succ y) = Minus y Minus x + Plus y = Plus y + Minus x instance CoSemigroup Nat instance CoSemigroup Integer instance CoMonoid Integer 0 = Zero instance CoGroup Integer - Plus x = Minus x - Minus x = Plus y - Zero = Zero instance CoAbelianGroup Integer instance Magma Integer x * Zero = Zero x * Plus One = x x * Plus (Succ y) = x + (x * y) x * Minus y = - (x * Plus y) instance Semigroup Integer instance Monoid Integer 1 = Plus One instance Ring Integer