aurorscript.js

aurorscript.js

"use strict";

// -- stdlib --
var pure = a=>_=>a                        // pure :: a -> IO a
var bind = m=>f=>_=>f(m())()              // bind :: IO a -> (a -> IO b) -> IO b
var exec = m=>m()                         // exec :: IO a -> a
var wrap = f=>a=>_=>f(a)                  // wrap :: (a -> b) -> (a -> IO b)
var put = wrap(console.log.bind(console)) // put :: a -> IO ()
var get = wrap(url=>{                     // get :: string -> IO string
    var xhr = new XMLHttpRequest()
    xhr.open("get", url, false)
    xhr.send()
    return xhr.responseText
})

// -- runtime --
Object.defineProperty(window, "main", { set: exec });


/*

A proof that (pure,bind) is a Monad:

law1:  (return x) >>= f == f x

  bind(pure(x))(f)
= (m=>f=>_=>f(m())())(pure(x))(f)
= (f=>_=>f(pure(x)())())(f)
= _=>f(pure(x)())()
= f((pure)(x)())
= f((a=>_=>a)(x)())
= f((_=>x)())
= f(x)

bind(pure(x))(f) = f(x)


law2:   m >>= return == m

  bind(m)(pure)
= (m=>f=>_=>f(m())())(m)(pure)
= (   f=>_=>f   (m())())   (pure)
= (      _=>pure(m())())
= (      _=>(a=>_=>a)(m())())
= (      _=>(_=>(m())) ())
= (      _=>((m())) )
= _=>(m())

bind(m)(pure)() = m()
bind(m)(pure) = m


law3:   (m >>= f) >>= g == m >>= (\x -> f x >>= g)

  bind(bind(m)(f))(g)
= bind(   bind                  (m)  (f)   )(g)
= bind(   (n=>h=>_=>h(n())())   (m)  (f)   )(g)
= bind(   (   h=>_=>h(m())())        (f)   )(g)
= bind    (      _=>f(m())())               (g)
= bind                       (_=>f(m())())   (g)
= (n=>h=>_=>h      (n())())  (_=>f(m())())   (g)
= (n=>h=>_=>h( n              ())())  (_=>f(m())())   (g)
= (   h=>_=>h( (_=>f(m())())  ())())                  (g)
= (      _=>g( (_=>f(m())())  ())())     
= (      _=>g(     f(m())()     )())     
= (_=>g(f(m())())())     

  bind(m)(x => bind(f(x))(g))
= bind(m)(x => (n=>h=>_=>h(n())()) (f(x))   (g))  
= bind(m)(x => (n=>h=>_=>h(n      ())()) (f(x))   (g))  
= bind(m)(x => (   h=>_=>h((f(x)) ())())          (g))  
= bind(m)(x => (   h=>_=>h((f(x)) ())())          (g))  
= bind(m)(x => (      _=>g((f(x)) ())())             )  
= bind(m)(x => (_=>g((f(x))())()))
= (n=>h=>_=>h(n())())   (m)   (x => (_=>g((f(x))())()))
= (   h=>_=>h(m())())         (x => (_=>g((f(x))())()))
= (   h=>_=>h                          (m())())  (x => (_=>g((f(x))())()))
= (      _=>(x => (_=>g((f(x))())()))  (m())())  
= (      _=>(x => (_=>g((f(x         ))())()))  (m())())  
= (      _=>(     (_=>g((f((m())     ))())()))       ())  
= (_=>((_=>g((f((m())))())()))())
= (_=>(_=>g(f(m())())())())
= (_=>g(f(m())())())

bind(bind(m)(f))(g) = bind(m)(x => bind(f(x))(g))
 */