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

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186
  1. // This file contains a wild collection examples of how Katrin code might look.
  2. // No "module" or "package" specification. Only the file name is used.
  3. // I might be clinging to Haskell syntax too much. I might need to get more independent.
  4. Type = Set Universe // The backend of this needs a lot of thought.
  5. Maybe _ : Type -> Type
  6. Maybe a = type
  7. Nothing : Maybe a
  8. Just : a → Maybe a
  9. (_,_) : Type → Type → Type // Underscore syntax shamelssly stolen from Agda. Very flexible.
  10. (a,b) = type
  11. (_,_) : a -> b -> (a,b)
  12. ℕ : Type
  13. ℕ = type
  14. One : ℕ
  15. Succ : ℕ → ℕ
  16. ℤ : Type
  17. ℤ = type
  18. Zero : ℤ
  19. Plus : ℕ → ℤ
  20. Minus : ℕ → ℤ
  21. Coℕ : Type
  22. Coℕ = cotype
  23. Pred : Coℕ → Maybe Coℕ
  24. Three : ℕ
  25. Three = Succ (Succ One)
  26. CoTwo : Coℕ
  27. CoTwo = {Pred = Just {Pred = Nothing}} // Provisional syntax borrowed from Haskell, I'll need to think of something better.
  28. _ coPlus _ : Coℕ → Coℕ → Coℕ // Defining pure text functions infix should probably give a warning.
  29. x coPlus y = case Pred y
  30. Just y' -> {Pred = Just x} coPlus y'
  31. // Lambda syntax ideas
  32. f _ : ℕ → ℕ
  33. f = x ↦ x + 10
  34. f = λx . x + 10
  35. f = \x . x + 10
  36. f = \x -> x + 10
  37. f = \x => x + 10
  38. List _ : Type → Type
  39. List a = type
  40. Empty : List a
  41. Cons : a → List a → List a
  42. CoList _ : Type → Type
  43. CoList a = cotype
  44. Split : CoList a → Maybe (a, CoList a)
  45. OneTwoThree : List Int
  46. OneTwoThree = Cons 1 (Cons 2 (Cons 3 Empty))
  47. CoOneTwoThree : CoList Int
  48. CoOneTwoThree = Just (1, Just (2, (Just 3, Nothing)))
  49. Nat : Type
  50. Nat = ℕ
  51. Pair _ _ : Set → Set → Set
  52. Pair a b = type
  53. Pair : (first : a) → (second : b) → Pair a b
  54. // Rethink this together with the Set/Type stuff
  55. Person : Set
  56. Person = {Alice, Bob}
  57. bestPair : Pair Person Person
  58. bestPair = Pair Alice Bob
  59. test : Set
  60. test = {Kek, Lel, Topkek}
  61. // Traits for algebraic structures for calculating.
  62. trait Magma a
  63. * : a → a → a
  64. trait (Magma a) ⇒ Semigroup a
  65. (x * y) * z == x * (y * z)
  66. trait (Semigroup a) ⇒ Monoid a
  67. 1 : a
  68. 1 * x == x
  69. x * 1 == x
  70. trait (Monoid a) ⇒ Group a
  71. 1/ _ : a → a
  72. trait (Group a) ⇒ AbelianGroup a
  73. x * y == y * x
  74. // Define all those analogously, but named "Co" and with + instead of *.
  75. // Is there a more elegant way?
  76. trait CoMagma a
  77. _ + _ : a → a → a
  78. trait (CoMagma a) ⇒ CoSemigroup a
  79. (x + y) + z == x + (y + z)
  80. trait (CoSemigroup a) ⇒ CoMonoid a
  81. 0 : a
  82. 0 + x == x
  83. x + 0 == x
  84. trait (CoMonoid a) ⇒ CoAbelianMonoid a
  85. x + y == y + x
  86. trait (CoMonoid a) ⇒ CoGroup a
  87. - _ : a → a
  88. trait (CoGroup a, CoAbelianMonoid a) ⇒ CoAbelianGroup a
  89. trait (Monoid a, CoAbelianMonoid a) ⇒ Semiring a
  90. x * (y + z) = (x * y) + (x * z)
  91. (y + z) * x = (y * x) + (z * x)
  92. trait (Semiring a, CoAbelianGroup a) ⇒ Ring a
  93. trait (Ring a, AbelianGroup a/0) ⇒ Field a
  94. // Probably using less mathematical and more concrete names would be a good idea.
  95. // Instances for ℕ and ℤ. This should make normale calculations using those types possible.
  96. instance CoMagma ℕ
  97. x + Zero = x
  98. x + (Succ y) = (Succ x) + y
  99. instance CoMagma ℤ
  100. x + Zero = x
  101. Zero + y = y
  102. Plus x + Plus y = x + y
  103. Minus x + Minus y = Minus (x + y)
  104. Plus (Succ x) + Minus One = Plus x
  105. Plus (Succ x) + Minus (Succ y) = Plus x + Minus y
  106. Plus One + Minus (Succ y) = Minus y
  107. Minus x + Plus y = Plus y + Minus x
  108. instance CoSemigroup ℕ
  109. instance CoSemigroup ℤ
  110. instance CoMonoid ℤ
  111. 0 = Zero
  112. instance CoGroup ℤ
  113. - Plus x = Minus x
  114. - Minus x = Plus y
  115. - Zero = Zero
  116. instance CoAbelianGroup ℤ
  117. instance Magma ℤ
  118. x * Zero = Zero
  119. x * Plus One = x
  120. x * Plus (Succ y) = x + (x * y)
  121. x * Minus y = - (x * Plus y)
  122. instance Semigroup ℤ
  123. instance Monoid ℤ
  124. 1 = Plus One
  125. instance Ring ℤ