thinking about IO

TODO.md

@@ -33,6 +33,7 @@
 - [x] implicit patterns
 - [x] operators
 - [x] pair syntax (via comma operator)
+- [ ] `data` sugar: `data Maybe a = Nothing | Just a`
 - [x] matching on operators
   - [x] top level
   - [x] case statements

newt/IO.newt

@@ -13,18 +13,32 @@ 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
+iobind ma mab = \ w => case ma w of
   (MkIORes a w) => mab a w
 
-_>>=_ : {a b : U} -> IO a -> (a -> IO b) -> IO b
+iopure : {a : U} -> a -> IO a
-_>>=_ = iobind
+iopure a = \ w => MkIORes a w
 
-infixr 2 _>>=_
+IOMonad : Monad IO
-infixr 2 _>>_
+IOMonad = MkMonad iobind iopure
 
--- FIXME - bad parse error for lambda without the parens
+data Unit : U where
+  MkUnit : Unit
 
-_>>_ :  {a b : U} -> IO a -> IO b -> IO b
+ptype String
-_>>_ ma mb = ma >>= (\ _ => mb)
 
+pfunc log : String -> IO Unit := "(s) => (w) => MkIORes(console.log(s),w)"
+
+-- this version wraps with IO, but leaves this plog in scope
+pfunc plog : String -> Unit := "(s) => console.log(s)"
+
+log2 : String -> IO Unit
+log2 s = pure $ plog s
+
+main : IO Unit
+main = do
+  log "woot"
+  log2 "line 2"

newt/Prelude.newt

@@ -20,3 +20,27 @@ infixr 0 _$_
 _$_ : {a b : U} -> (a -> b) -> a -> b
 f $ a = f a
 
+
+-- Monad
+
+-- 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
+
+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
+
+_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> 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
+
+-- IO
+
+

src/Main.idr

@@ -43,7 +43,9 @@ writeSource fn = do
   docs <- compile
   let src = unlines $ ["#!/usr/bin/env node"]
         ++ map (render 90) docs
-        ++ [ "main();" ]
+        ++ [ "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })"
+           , "main();"
+           ]
   Right _ <- writeFile fn src
     | Left err => fail (show err)
   Right _ <- chmodRaw fn 493 | Left err => fail (show err)