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 3.8KB Permalink History Raw

 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186 // 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. Type = Set Universe // The backend of this needs a lot of thought. Maybe _ : Type -> Type Maybe a = type Nothing : Maybe a Just : a → Maybe a (_,_) : Type → Type → Type // Underscore syntax shamelssly stolen from Agda. Very flexible. (a,b) = type (_,_) : a -> b -> (a,b) ℕ : Type ℕ = type One : ℕ Succ : ℕ → ℕ ℤ : Type ℤ = type Zero : ℤ Plus : ℕ → ℤ Minus : ℕ → ℤ Coℕ : Type Coℕ = cotype Pred : Coℕ → Maybe Coℕ Three : ℕ Three = Succ (Succ One) CoTwo : Coℕ CoTwo = {Pred = Just {Pred = Nothing}} // Provisional syntax borrowed from Haskell, I'll need to think of something better. _ coPlus _ : Coℕ → Coℕ → Coℕ // Defining pure text functions infix should probably give a warning. x coPlus y = case Pred y Just y' -> {Pred = Just x} coPlus y' // Lambda syntax ideas f _ : ℕ → ℕ f = x ↦ x + 10 f = λx . x + 10 f = \x . x + 10 f = \x -> x + 10 f = \x => x + 10 List _ : Type → Type List a = type Empty : List a Cons : a → List a → List a CoList _ : Type → Type CoList a = cotype Split : CoList a → Maybe (a, CoList a) 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 = ℕ 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? 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 ℕ and ℤ. This should make normale calculations using those types possible. instance CoMagma ℕ x + Zero = x x + (Succ y) = (Succ x) + y instance CoMagma ℤ 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 ℕ instance CoSemigroup ℤ instance CoMonoid ℤ 0 = Zero instance CoGroup ℤ - Plus x = Minus x - Minus x = Plus y - Zero = Zero instance CoAbelianGroup ℤ instance Magma ℤ x * Zero = Zero x * Plus One = x x * Plus (Succ y) = x + (x * y) x * Minus y = - (x * Plus y) instance Semigroup ℤ instance Monoid ℤ 1 = Plus One instance Ring ℤ