242 lines
6.3 KiB
Agda
242 lines
6.3 KiB
Agda
|
||
|
||
/-
|
||
Ok, so this is newt, a dependent typed programming language that
|
||
I am implementing to learn how they work. It targets javascript
|
||
and borrows a lot of syntax from Idris and Agda.
|
||
|
||
This page is a very simple web playground based on the monaco editor.
|
||
It runs newt, compiled by Idris2, in a web worker.
|
||
|
||
Block comments follow Lean because they're easier to type on a
|
||
US keyboard.
|
||
|
||
The output, to the right, is somewhat noisy and obtuse. You'll see
|
||
INFO and sometimes ERROR messages that show up in the editor view
|
||
on hover. I'm emitting INFO for solved metas.
|
||
|
||
The Day1.newt and Day2.newt are last year's advent of code, translated
|
||
from Lean.
|
||
|
||
-/
|
||
|
||
-- One-line comments begin with two hyphens
|
||
|
||
-- every file begins with a `module` declaration
|
||
-- it must match the filename
|
||
module Tour
|
||
|
||
-- We can import other modules, with a flat namespace and no cycles,
|
||
-- diamonds are ok
|
||
|
||
-- commented out until we preload other files into the worker
|
||
-- import Lib
|
||
|
||
-- We're calling the universe U and are doing type in type for now
|
||
|
||
-- Inductive type definitions are similar to Idris, Agda, or Haskell
|
||
data Nat : U where
|
||
Z : Nat
|
||
S : Nat -> Nat
|
||
|
||
-- Multiple names are allowed on the left:
|
||
data Bool : U where
|
||
True False : Bool
|
||
|
||
-- function definitions are equations using dependent pattern matching
|
||
plus : Nat -> Nat -> Nat
|
||
plus Z m = m
|
||
plus (S n) m = S (plus n m)
|
||
|
||
-- we can also have case statements on the right side
|
||
-- the core language includes case statements
|
||
-- here `\` is used for a lambda expression:
|
||
plus' : Nat -> Nat -> Nat
|
||
plus' = \ n m => case n of
|
||
Z => m
|
||
S n => S (plus' n m)
|
||
|
||
-- We can define operators. Mixfix is supported, but we don't
|
||
-- allow ambiguity (so you can't have both [_] and [_,_]). See
|
||
-- the Reasoning.newt sample for a mixfix example.
|
||
infixl 2 _≡_
|
||
|
||
-- Here is an equality, like Idris, everything goes to the right of the colon
|
||
-- Implicits are denoted with braces `{ }`
|
||
-- unlike idris, you have to declare all of your implicits
|
||
data _≡_ : {A : U} -> A -> A -> U where
|
||
Refl : {A : U} {a : A} -> a ≡ a
|
||
|
||
-- And now the compiler can verify that 1 + 1 = 2
|
||
test : plus (S Z) (S Z) ≡ S (S Z)
|
||
test = Refl
|
||
|
||
-- Ok now we do typeclasses. `class` and `instance` are sugar for
|
||
-- ordinary data and functions:
|
||
|
||
-- Let's say we want a generic `_+_` operator
|
||
infixl 7 _+_
|
||
|
||
class Add a where
|
||
_+_ : a -> a -> a
|
||
|
||
instance Add Nat where
|
||
Z + m = m
|
||
(S n) + m = S (n + m)
|
||
|
||
-- and it now finds the implicits, you'll see the solutions to the
|
||
-- implicits if you hover over the `+`.
|
||
two : Nat
|
||
two = S Z + S Z
|
||
|
||
-- We can leave a hole in an expression with ? and the editor will show us the
|
||
-- scope and expected type (hover to see)
|
||
foo : Nat -> Nat -> Nat
|
||
foo a b = ?
|
||
|
||
-- Newt compiles to javascript, there is a tab to the right that shows the
|
||
-- javascript output. It is not doing erasure (or inlining) yet, so the
|
||
-- code is a little verbose.
|
||
|
||
-- We can define native types, if the type is left off, it defaults to U
|
||
|
||
ptype Int : U
|
||
ptype String : U
|
||
ptype Char : U
|
||
|
||
-- The names of these three types are special, primitive numbers, strings,
|
||
-- and characters inhabit them, respectively. We can match on primitives, but
|
||
-- must provide a default case:
|
||
|
||
isVowel : Char -> Bool
|
||
isVowel 'a' = True
|
||
isVowel 'e' = True
|
||
isVowel 'i' = True
|
||
isVowel 'o' = True
|
||
isVowel 'u' = True
|
||
isVowel _ = False
|
||
|
||
-- And primitive functions have a type and a javascript definition:
|
||
|
||
pfunc plusInt : Int -> Int -> Int := `(x,y) => x + y`
|
||
pfunc plusString : String -> String -> String := `(x,y) => x + y`
|
||
|
||
-- We can make them Plus instances:
|
||
|
||
|
||
instance Add Int where
|
||
_+_ = plusInt
|
||
|
||
instance Add String where
|
||
_+_ = plusString
|
||
|
||
concat : String -> String -> String
|
||
concat a b = a + b
|
||
|
||
-- Now we define Monad
|
||
class Monad (m : U -> U) where
|
||
pure : {a} -> a -> m a
|
||
bind : {a b} -> m a -> (a -> m b) -> m b
|
||
|
||
/-
|
||
This desugars to:
|
||
|
||
data Monad : (m : U -> U) -> U where
|
||
MkMonad : {m : U -> U} ->
|
||
(pure : {a : _} -> a -> m a) ->
|
||
(bind : {a : _} -> {b : _} -> m a -> a -> m b -> m b) ->
|
||
Monad m
|
||
|
||
pure : {m : U -> U} -> {{_ : Monad m}} -> {a : _} -> a -> m a
|
||
pure {m} {{MkMonad pure bind}} = pure
|
||
|
||
bind : {m : U -> U} -> {{_ : Monad m}} -> {a : _} -> {b : _} -> m a -> a -> m b -> m b
|
||
bind {m} {{MkMonad pure bind}} = bind
|
||
|
||
-/
|
||
|
||
-- we can declare multiple infix operators at once
|
||
infixl 1 _>>=_ _>>_
|
||
|
||
_>>=_ : {m} {{Monad m}} {a b} -> m a -> (a -> m b) -> m b
|
||
_>>=_ ma amb = bind ma amb
|
||
|
||
_>>_ : {m} {{Monad m}} {a b} -> m a -> m b -> m b
|
||
ma >> mb = ma >>= (λ _ => mb)
|
||
|
||
-- Now we define list and show it is a monad. At the moment, I don't
|
||
-- have sugar for Lists,
|
||
|
||
infixr 3 _::_
|
||
data List : U -> U where
|
||
Nil : ∀ A. List A
|
||
_::_ : ∀ A. A -> List A -> List A
|
||
|
||
infixr 7 _++_
|
||
_++_ : ∀ a. List a -> List a -> List a
|
||
Nil ++ ys = ys
|
||
(x :: xs) ++ ys = x :: (xs ++ ys)
|
||
|
||
instance Monad List where
|
||
pure a = a :: Nil
|
||
bind Nil f = Nil
|
||
bind (x :: xs) f = f x ++ bind xs f
|
||
|
||
/-
|
||
This desugars to: (the names in guillemots are not user-accessible)
|
||
|
||
«Monad List,pure» : { a : U } -> a:0 -> List a:1
|
||
pure a = _::_ a Nil
|
||
|
||
«Monad List,bind» : { a : U } -> { b : U } -> (List a) -> (a -> List b) -> List b
|
||
bind Nil f = Nil bind (_::_ x xs) f = _++_ (f x) (bind xs f)
|
||
|
||
«Monad List» : Monad List
|
||
«Monad List» = MkMonad «Monad List,pure» «Monad List,bind»
|
||
|
||
-/
|
||
|
||
-- We'll want Pair below. `,` has been left for use as an operator.
|
||
-- Also we see that → can be used in lieu of ->
|
||
infixr 1 _,_ _×_
|
||
data _×_ : U → U → U where
|
||
_,_ : ∀ A B. A → B → A × B
|
||
|
||
-- The _>>=_ operator is used for desugaring do blocks
|
||
|
||
prod : ∀ A B. List A → List B → List (A × B)
|
||
prod xs ys = do
|
||
x <- xs
|
||
y <- ys
|
||
pure (x, y)
|
||
|
||
-- The playground is compiling to javascript and will give an error if
|
||
-- main isn't implemented, so I'll crib the definition of IO from
|
||
-- Prelude:
|
||
|
||
data Unit : U where
|
||
MkUnit : Unit
|
||
|
||
ptype World
|
||
|
||
data IORes : U -> U where
|
||
MkIORes : ∀ a. a -> World -> IORes a
|
||
|
||
IO : U -> U
|
||
IO a = World -> IORes a
|
||
|
||
instance Monad IO where
|
||
bind ma mab = \ w => case ma w of
|
||
MkIORes a w => mab a w
|
||
pure a = \ w => MkIORes a w
|
||
|
||
-- Here we declare `uses` to let the dead code elimination know we're poking
|
||
-- at MKIORes and MkUnit behind the compiler's back.
|
||
pfunc putStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
|
||
console.log(s)
|
||
return MkIORes(undefined,MkUnit,w)
|
||
}`
|
||
|
||
main : IO Unit
|
||
main = putStrLn "hello, world"
|