Some monads without higher-order functions

57 views
Skip to first unread message

Artyom Shalkhakov

unread,
Dec 31, 2014, 10:40:46 AM12/31/14
to ats-lan...@googlegroups.com
Here's something a came up with:

https://gist.github.com/ashalkhakov/5a36de12a2c6750c46ae

This shows a Maybe monad from Haskell in ATS/Postiats. The idea is that no higher-order functions are involved (and no closures too). If it works, then it means we have several intresting possibilities to explore: for instance, we can build F# Async-like computations in ATS without much runtime overhead.

Does anybody have a working patsopt to compile this code and run it? All I know is that it type-checks.
Message has been deleted

gmhwxi

unread,
Dec 31, 2014, 7:44:51 PM12/31/14
to ats-lan...@googlegroups.com

The idea is okay in principle. However, there are several issues that
need to be addressed. Basically, the way in which templates are expanded in
ATS2 is not precisely like what you might have thought.

Here is a working version:


(* ****** ****** *)
 
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
 
(* ****** ****** *)

// the interface
 
abst@ype M
(t@ype) = ptr
 
extern
fun
{a:t@ype}
ret
: a -> M(a)
 
extern
fun
{a,b:t@ype}
bind
: M(a) -> M(b)
 
symintr
>>=
postfix
>>=
overload
>>= with bind
 
// we replace the second argument of bind with a function template
// which should allow the ATS compiler to inline aggressively
extern
fun
{a,b:t@ype}
bind$cont
(x: a): M(b)
 
(* ****** ****** *)

extern
fun
{a,b:t@ype}
bind1
: M(a) -> M(b)
extern
fun
{a,b:t@ype}
bind2
: M(a) -> M(b)

(* ****** ****** *)

// one possible implementation
 
assume M
(a:t@ype) = Option a
 
// an explicit failure function (cf. MonadFail)
fun
Mfail {a:t@ype} (): M(a) = None ()
 
implement
{a}(*tmp*)
ret
(x) = Some x
 
implement
{a,b}
bind
(x) = let
//
val
() = println! ("bind: x = ...")
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind]
 
(* ****** ****** *)

implement
{a,b}
bind1
(x) = let
//
val
() = println! ("bind1: x = ...")
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind1]
 
(* ****** ****** *)

implement
{a,b}
bind2
(x) = let
//
val
() = println! ("bind2: x = ...")
//
in
//
case+ x of
| Some x => bind$cont<a,b>(x) | None () => None ()
//
end // end of [bind2]
 
(* ****** ****** *)

// a Maybe monad can be run
fun
{a:t@ype} runM (x : M(a)): a =
case+ x of
| Some x => x
| None () => exit_errmsg (1, "runM failed!")
 
(* ****** ****** *)
(*
// usage example
// this computation doesn't know anything about the internals
// of the implementation of the underlying monad, I think
fun test
(x : int): M int =
ret
5 >>= where {implement bind$cont<int,int> (y) =
ret
4 >>= where {implement bind$cont<int,int> (z) =
ret
(x + y + z)}}
*)
(*
fun test
(x : int): M int =
bind
<int,int>(ret(5)) where {implement bind$cont<int,int> (y) =
bind
<int,int>(ret(4)) where {implement bind$cont<int,int> (z) =
ret
(x + y + z)}}
*)
(*
fun test
(x : int): M int = ret(x)
*)
(*
fun
test
(x : int): M int =
bind
<int,int>(ret(10)) where
{
implement bind$cont
<int,int> (y) = ret (x + y)
}
*)

fun
test
(
  x
: int
) : M int = let
//
implement
bind$cont
<int,int> (y) = let
//
val
() = println! ("bind$cont(1): y = ", y)
//
implement
bind$cont
<int,int> (z) = let
//
val
() = println! ("bind$cont: 2") in ret (x + y + z)
//
end // end of [bind$cont]
//
in
  bind1
<int,int> (ret(10))
end // end of [bind$cont]
//
in
  bind2
<int,int> (ret(100))
end // end of [test]
 
(* ****** ****** *)
 
implement
main0
(argc, argv) = let
val comp
= test (argc)
// specify the type explicitly
val res
= runM<int> (comp)
in
  println
!("result = ", res);
end // end of [main]

(* ****** ****** *)

Artyom Shalkhakov

unread,
Dec 31, 2014, 10:57:00 PM12/31/14
to ats-lan...@googlegroups.com
On Thursday, January 1, 2015 6:44:51 AM UTC+6, gmhwxi wrote:

The idea is okay in principle. However, there are several issues that
need to be addressed. Basically, the way in which templates are expanded in
ATS2 is not precisely like what you might have thought.


Thanks!

The takeaway, IIUC, is that for templates to work in this case, the user has to specify template parameters (in angular braces) in all template function applications.
 

gmhwxi

unread,
Dec 31, 2014, 11:37:08 PM12/31/14
to ats-lan...@googlegroups.com

I would just use the standard style.
'gcc -O3' should eliminate actual closure formation.
You still need -DATS_MEMALLOC_LIBC because option-values
are heap-allocated.


(* ****** ****** *)
//
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)


abst@ype M
(t@ype) = ptr

extern
fun
{a:t@ype}
ret
: a -> M(a)

extern
fun
{a,b:t@ype}

bind
: (M(a), a -<cloref1> M(b)) -> M(b)

(* ****** ****** *)

local


assume M
(a:t@ype) = Option a

in (* in-of-local *)


implement
{a}(*tmp*)
ret
(x) = Some x

implement
{a,b}

bind
(x, f) = let
//
val
() = println! ("bind: x = ...")
//
in
//
case+ x of
| Some x => f (x) | None () => None ()

//
end // end of [bind]


fun
{a:t@ype}

runM
(x : M(a)): a =
case+ x of
| Some x => x
| None () => exit_errmsg (1, "runM failed!")

end // end of [local]

(* ****** ****** *)

infix
>>=


(* ****** ****** *)
//
extern
fun
mytest
 
(x: int) : M(int) = "mytest"
//
implement
mytest
(x) = let
//
macdef
>>=(x, f) = bind<int,int>(,(x), ,(f))
//
in
//
ret
(10)
>>= (lam(y) =>
ret
(100)
>>= (lam(z) =>

ret
(x + y + z)
)
)
//

end // end of [test]

(* ****** ****** *)

implement
main0
(argc, argv) =
let
val comp
= mytest (argc)

// specify the type explicitly
val res
= runM<int> (comp)
in
  println
!("result = ", res);
end // end of [main]

(* ****** ****** *)

gmhwxi

unread,
Jan 1, 2015, 1:10:46 AM1/1/15
to ats-lan...@googlegroups.com
I added some code to show that (original) Haskell-like syntax for using monads can be simulated
in ATS (to a large degree):

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/ATSLIB/libats_ML_monad_maybe.dats

When you write

ret(x) >>= (lam (y) => ...) // >>= is infix for bind

'gcc-O3' should be able to optimize away the need to actually form a closure to pass to >>= as long as
the definition of >>= is available.
...
Reply all
Reply to author
Forward
0 new messages