diff --git a/playground/samples/Tour.newt b/playground/samples/Tour.newt index b0195e3..23248b8 100644 --- a/playground/samples/Tour.newt +++ b/playground/samples/Tour.newt @@ -95,8 +95,9 @@ 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. +-- javascript output. There is some erasure, but inlining is not being done +-- yet. Dead code elimination will be done if there is a `main` function. +-- That is not the case in this file. -- We can define native types, if the type is left off, it defaults to U @@ -210,32 +211,3 @@ prod xs ys = do 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"