From 9b19c569c9d52f1d34f223e70f55bce16511ffc0 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 19 Nov 2024 05:35:14 -0800 Subject: [PATCH] sugar in samples --- TODO.md | 6 +- playground/build | 6 +- port/Prelude.newt | 162 ++++++++++++++++------------------------------ 3 files changed, 60 insertions(+), 114 deletions(-) diff --git a/TODO.md b/TODO.md index ddf4a79..3a79a01 100644 --- a/TODO.md +++ b/TODO.md @@ -1,8 +1,6 @@ ## TODO -NOW - sorting out instance sugar for `Monad {a} -> (Either a)`. - - [ ] accepting DCon for another type (skipping case, but should be an error) - [ ] don't allow (or dot) duplicate names on LHS - [ ] remove metas from context, M has TopContext @@ -17,11 +15,11 @@ NOW - sorting out instance sugar for `Monad {a} -> (Either a)`. - Handles the forward decl in `Zoo1.newt`, but we'll need different syntax if we have different core terms for TCon/DCon/Function - [ ] Require infix decl before declaring names with `_` (helps find bugs) -- [ ] sugar for typeclasses +- [x] sugar for typeclasses - [ ] maybe add implicits in core to help resugar operators? - There is also a bit where kovacs uses the implicit on the type (a value) to decide to insert - [ ] consider binders in environment, like Idris, to better mark `let` and to provide names -- [ ] move some top-level chattiness to `debug` +- [x] move some top-level chattiness to `debug` - [ ] consider optionally compiling to eliminators for a second type-checking pass to help catch bugs. - [x] Allow unicode operators/names - Web playground diff --git a/playground/build b/playground/build index b06302b..9fca0f0 100755 --- a/playground/build +++ b/playground/build @@ -1,9 +1,9 @@ #!/bin/sh -echo monaco worker +echo build monaco worker esbuild --bundle node_modules/monaco-editor/esm/vs/editor/editor.worker.js > public/workerMain.js -echo newt worker +echo build newt worker esbuild src/worker.ts > public/worker.js -echo newt +echo copy newt cat ../build/exec/newt.js |grep -v '^#'>> public/worker.js cp samples/* public # esbuild --minify ../build/exec/newt.min.js > public/newt.js diff --git a/port/Prelude.newt b/port/Prelude.newt index f75dc9e..06c3b70 100644 --- a/port/Prelude.newt +++ b/port/Prelude.newt @@ -60,45 +60,28 @@ infixr 2 _,_ data _×_ : U → U → U where _,_ : {A B} → A → B → A × B - infixl 6 _<_ -data Ord : U → U where - MkOrd : {A} → (A → A → Bool) → Ord A +class Ord a where + _<_ : a → a → Bool -_<_ : {A} {{Ord A}} → A → A → Bool -_<_ {{MkOrd cmp}} a b = cmp a b - -cmpNat : Nat → Nat → Bool -cmpNat Z Z = True -cmpNat Z m = False -cmpNat n Z = True -cmpNat (S n) (S m) = True - -OrdNat : Ord Nat -OrdNat = MkOrd cmpNat +instance Ord Nat where + _ < Z = False + Z < S _ = True + S n < S m = n < m -- Monad --- TODO sugar for if then else (mixfix is too eager) - --- TODO stack with Applicative, etc? - -data Monad : (U -> U) -> U where - MkMonad : { M : U -> U } -> - (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) -> - (pure : {A : U} -> A -> M A) -> - Monad M +class Monad (m : U → U) where + bind : {a b} → m a → (a → m b) → m b + pure : {a} → a → m a infixl 1 _>>=_ _>>_ -_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b -_>>=_ {a} {b} {m} {{MkMonad bind' _}} ma amb = bind' {a} {b} ma amb +_>>=_ : {m} {{Monad m}} {a b} -> (m a) -> (a -> m b) -> m b +ma >>= amb = bind ma amb -_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b +_>>_ : {m} {{Monad m}} {a b} -> m a -> m b -> m b ma >> mb = mb -pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a -pure {_} {_} {{MkMonad _ pure'}} a = pure' a - -- Equality infixl 1 _≡_ @@ -114,89 +97,47 @@ sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a sym Refl = Refl -- Functor -data Functor : (U → U) → U where - MkFunctor : {m : U → U} → ({a b : U} → (a → b) → m a → m b) → Functor m -map : {m} {{Functor m}} → {a b} → (a → b) → m a → m b -map {{MkFunctor f}} ma = f ma +class Functor (m : U → U) where + map : {a b} → (a → b) → m a → m b infixr 4 _<$>_ -_<$>_ : {f : U → U} {{Functor f}} {a b} → (a → b) → f a → f b +_<$>_ : {f} {{Functor f}} {a b} → (a → b) → f a → f b f <$> ma = map f ma - -mapMaybe : {a b} → (a → b) → Maybe a → Maybe b -mapMaybe f Nothing = Nothing -mapMaybe f (Just a) = Just (f a) - -FunctorMaybe : Functor Maybe -FunctorMaybe = MkFunctor mapMaybe - - - --- Idris is lazy in second arg, we don't have that. -data Alternative : (U → U) → U where - MkAlt : {m : U → U} → - ({a} → m a → m a → m a) → - Alternative m +instance Functor Maybe where + map f Nothing = Nothing + map f (Just a) = Just (f a) infixr 2 _<|>_ -_<|>_ : {m : U → U} {{Alternative m}} → {a} → m a → m a → m a -_<|>_ {m} {{MkAlt f}} {a} x y = f x y +class Alternative (m : U → U) where + _<|>_ : {a} → m a → m a → m a -altMaybe : {a} → Maybe a → Maybe a → Maybe a -altMaybe Nothing x = x -altMaybe (Just x) _ = Just x - -AltMaybe : Alternative Maybe -AltMaybe = MkAlt altMaybe +instance Alternative Maybe where + Nothing <|> x = x + Just x <|> _ = Just x -- Semigroup infixl 8 _<+>_ -data Semigroup : U → U where - MkSemi : {a} → (a → a → a) → Semigroup a - -_<+>_ : {a} {{Semigroup a}} → a → a → a -_<+>_ {{MkSemi op}} x y = op x y - +class Semigroup a where + _<+>_ : a → a → a infixl 7 _+_ -data Add : U → U where - MkAdd : {A} → (A → A → A) → Add A - -_+_ : {A} {{Add A}} → A → A → A -_+_ {{MkAdd add}} x y = add x y +class Add a where + _+_ : a → a → a infixl 8 _*_ -data Mul : U → U where - MkMul : {A} → - (A → A → A) → - Mul A +class Mul a where + _*_ : a → a → a -_*_ : {A} {{Mul A}} → A → A → A -_*_ {{MkMul mul}} x y = mul x y - - --- TODO codata/copatterns might be nice here? --- AddNat : AddNat --- AddNat .add Z m = m --- AddNat .add (S n) m = S (self .add n m) - -addNat : Nat → Nat → Nat -addNat Z m = m -addNat (S n) m = S (addNat n m) - -AddNat : Add Nat -AddNat = MkAdd addNat - -mulNat : Nat → Nat → Nat -mulNat Z _ = Z -mulNat (S n) m = m + mulNat n m - -MulNat : Mul Nat -MulNat = MkMul mulNat +instance Add Nat where + Z + m = m + S n + m = S (n + m) +instance Mul Nat where + Z * _ = Z + S n * m = m + n * m -- TODO Sub infixl 7 _-_ @@ -205,6 +146,9 @@ Z - m = Z n - Z = n S n - S m = n - m +infixr 7 _++_ +class Concat a where + _++_ : a → a → a ptype String ptype Int @@ -217,6 +161,12 @@ pfunc length : String → Nat := "(s) => { return rval }" + + +pfunc sconcat : String → String → String := "(x,y) => x + y" +instance Concat String where + _++_ = sconcat + data Unit : U where MkUnit : Unit @@ -239,8 +189,7 @@ pfunc aempty : {a : U} -> Unit -> Array a := "() => []" pfunc fastConcat : List String → String := "(xs) => listToArray(undefined, xs).join('')" pfunc replicate : Nat -> Char → String := "() => abort('FIXME replicate')" - - +-- I don't want to use an empty type because it would be a proof of void ptype World data IORes : U -> U where @@ -249,16 +198,15 @@ data IORes : U -> U where IO : U -> U IO a = World -> IORes a --- TODO - if I move w to the left, I get "extra pattern variable" --- because I'm not looking instide the IO b type, probably should force it. -iobind : {a b : U} -> IO a -> (a -> IO b) -> IO b -iobind ma mab = \ w => case ma w of - (MkIORes a w) => mab a w - -iopure : {a : U} -> a -> IO a -iopure a = \ w => MkIORes a w - -IOMonad : Monad IO -IOMonad = MkMonad iobind iopure +instance Monad IO where + bind ma mab = \ w => case ma w of + MkIORes a w => mab a w + pure a = \ w => MkIORes a w pfunc putStrLn : String -> IO Unit := "(s) => (w) => console.log(s)" + +class Show a where + show : a → String + +instance Show String where + show a = a