Template-based implementation for functors

[gmhwxi]

If we box everything, then implementing functors (as is defined in Haskell) is straightforward
in ATS. However, for performance, one may not want to box everything. I sketched a template-based
implementation for functors as follows:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats

It should be fun and very useful to support linear functors (e.g., List0_vt).

Cheers!

--Hongwei

[August Alm]

I liked the sort of reversed perspective! Two objects A and B define a "for all functors F, F_map : F(A) -> F(B)". But having to pass around "F_name" and introduce a "FUNCTOR_F_elim" seems a bit heavy-handed. Or is there a possibility that the proof terms can be passed implicitly, like [pfgc: mfree_gc_v(l)] sometimes can? Could you say a bit more about the perceived benefits over the more traditional approach that you used in the Yoneda-code, where a functor is an [F: t0p -> type] together with an

F_map: {a, b: t0p} cfun(a, b) -> cfun(F(a), F(b))

?

[August Alm]

I guess what I really wanted to ask is: Why not just use an abstract [FUNCTOR(ftype)] instead of [FUNCTOR(fname: type, ftype), i.e., why insist on names?

[August Alm]

For fun and learning I tried to do linear monads in a similar spirit, see: https://glot.io/snippets/eogc8rdiv1 I get the code
to compile (without the test-case at the end which I've commented out; don't know what's wrong with that)
but it does not run on glot.io, because of LIBATS/ML-dependency and (I think) unboxed types. My take
does not involve "name-types", just abstract proofs that an [m: vt0ype -> vtype] is a monad.

Den onsdag 29 mars 2017 kl. 16:38:00 UTC+2 skrev gmhwxi:

[gmhwxi]

Unfortunately, using a type function (of the sort ftype or fvtype) as a
template argument is currently not supported. That is why I used a "name"
in my tempfunctor example. I just added some testing code:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats

[August Alm]

I see. Maybe a clever macro or something could remove the need for the user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype f_name" for each functor instance?

[gmhwxi]

I see. Maybe a clever macro or something could remove the need for the user to explicitly define "extern praxis FUNCTOR_f_elim" and "abstype f_name" for each functor instance?

Something can definitely done along this line. At some point in the past,
I was even contemplating some kind of support for automatically synthesizing
proofs of certain props. Kind of like inferring dictionaries for type classes.

I did not go forward right away because I wanted to see more use cases involving
concepts from category theory.
 

[August Alm]

I had another go at linear monads in the style of your template functors, see https://glot.io/snippets/eogc8rdiv1
The code typechecks but does not compile. The compiler indicates that I have undeclared templates, but I can't
figure out which/what that refers to, despite meticulously type-annotating everything.

If I can get this working then I'll try to expand it by implementing (linear) versions of the more common monads. Maybe add
comonads. It should not be too difficult once the core is functioning. I imagine it can become a small "showroom" to lure
other Haskell- and Scala(z)-programmers to ATS. (Real world use cases would be even nicer, but I don't feel like I have the
skills for that yet.)

[August Alm]

Sorry, wrong link. Here is the right one: https://glot.io/snippets/eoh28sd2p4

Den torsdag 30 mars 2017 kl. 15:54:08 UTC+2 skrev gmhwxi:

[gmhwxi]

I'll take a more careful look later.

For the moment, please:

val xs: list_vt(int_vt, 3) = $list_vt(I(1), I(2), I(3))

changes to

val xs = $list_vt{int_vt}(I(1), I(2), I(3))

[August Alm]

I think the problem is with

  extern fun{a, s: vt0ype}
  mapM_list_vt$fopr(a): s

It doesn't seem to work implementing it with [s=m(b)] (though it passes typechecking). But if I do

  extern fun{a, b: vt0ype}
  {m: fvtype}
  mapM_list_vt$fopr(a): m(b)

or

  extern fun{m_name: type}{a, b: vt0ype}
  {m: fvtype}
  mapM_list_vt$fopr(MONAD(m_name, m)| a): m(b)

then I don't even pass typechecking -- the compiler can't infer that the [m] in [mapM_list_vt$fopr] can
be identified with the [m] in [mapM_list_vt] (even if I type annotate with [mapM_list_vt$fopr<m_name><a, b>{m}).
Is there a way to coerce the typechecking in situations like this?

Best,
August

[Hongwei Xi]

If you change the body of mapM_list_vt_fun as follows:

    let
    implement(a,s)
    mapM_list_vt$fopr<a,s>(x) =
    let val x = $UN.castvwtp0(x) in $UN.castvwtp0(fopr(x)) end
    in mapM_list_vt$aux<m_name><a, b>{m}{n}(pfm| xs) end

then the code compiles. I saw the following lines after execution:
1
2
3

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/23c426ce-58fb-46f4-aa78-5644928808d8%40googlegroups.com.

[August Alm]

Great! But ...What just happened, what's the lesson I should take away?

"mapM" for the "option" monad is already quite handy, I think. Instead of a list of optional values one gets an optional list. Good for handling failure.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

[gmhwxi]

In the following code: the 'm' in m(b) is different from the 'm' in {m}:

  let implement mapM_list_vt$fopr<a, m(b)>(x) = fopr(x)

  in mapM_list_vt$aux<m_name><a, b>{m}{n}(pfm| xs) end

So the implementation of mapM_list_vt$fopr cannot be used for the purpose
of compiling mapM_list_vt$aux.

[August Alm]

Hrrm. So template terms in "<...>" are not restricted to the scope where you implement the template, but rather look at the scope where
the template interface was given? Otherwise I don't understand, as I can only see one 'm' in the scope of the whole "let.." (the 'm'
quantified "{m_ fvtype}" over in the type declaration).

By the way, in my current implementation of linear monads the "bind" function takes a "cloref1" function [fopr: cfun(a, m(b))]
as argument. Is this morally correct or would it be more interesting/useful to have [fopr: cloptr(a, m(b))]? I guess "cloptr" functions
could be handled the way it is, by taking out the "cloref1", applying the monadic bind, and putting the result back with the viewpart.
However, that would probably involve a fair bit of book-keeping and one of the things I am hoping to achieve is to reduce the amount of
book-keeping by tucking it away in a library of some standard monadic functions.

[gmhwxi]

When the following instance is compiled:

mapM_list_vt$aux<m_name><a, b>{m}{n}(pfm | xs)

The (instance) call to mapM_list_vt$fopr (in the body of mapM_list_vt$aux)
has the template parameter <a, m(b)> where the 'm' is from {m}. This call cannot
be compiled as no template implementation for mapM_list_vt$fopr can be used to
produce such an instance.

[gmhwxi]

cloref1 vs. cloptr1:

I would say that using cloref1 is okay. At least for moment.
Otherwise, the complexity you face can quickly be out of control.

[August Alm]

I got it working with linear types and cloptr functions, see
https://github.com/August-Alm/ATS-Experiments/blob/master/linear_monads.dats
(I can't get the code to work on glot.io unfortunately.) This is fun!

[gmhwxi]

I must say that I made a mistake. My early explanation was incorrect.
The code should have compiled. I will see if I can figure out the cause for this bug.

[gmhwxi]

Sorry. I got confused :(

My early explanation was actually correct.

Following is the header from mapM_list_vt$aux

  fun{m_name: type}{a, b: vt0ype}

  mapM_list_vt$aux
  {m: fvtype}
  {n: int}
  ( pfm: MONAD(m_name, m)
  | xs: list_vt(INV(a), n) ):
  m(list_vt(b, n)) =

When mapM_list_vt$aux is compiled. {m:fvtype} is not instantiated.
Only template parameters are instantiated. This is a big limitation of
the template system in ATS: Templates and polymorphism often do not
go well together.

[gmhwxi]

Cool!

You could just use int for int_vt, right? Maybe you also wanted
to try datavtype in this experiment.

[August Alm]

Actually, no, it will not compile with [int] instead of [int_vt]. I can't figure out
where in the code the problem appears; the compiler says

warning: cast to pointer from integer of different size [-Wint-to-pointer-cast]

I am guessing this is due to my hack of using [$UN.castvwtp0{ptr]] to evade scope restriction
for lambdas. Is that a good guess?

[August Alm]

Yes, that casting was the culprit. I managed to fix it. Actually, using cloptr functions throughout
made the code simpler, if anything, because it removed the need for such casting in most cases!
I also discovered that "where" works better than "let" in this specific situation.

[August Alm]

I don't understand, or maybe I understand the problem but not the solution
you offered with unsafe casts. I just tried implementing "foldM" (monadic
left fold) using the same tactic, but it is not working. Here is what I have:

         extern fun{a, b, s: vt0ype}  // [s = m(a)] in implementation!
         foldM_list_vt$fopr(a, b): s

        
         fun{m_name: type}{a, b: vt0ype}

         foldM_list_vt$aux

         {m: fvtype}
         {n: int}
         ( pfm: MONAD(m_name, m)

         | xs: list_vt(a, n)
         , init: b ):
         m(b) =
           case xs of
           | ~list_vt_nil() => monad_return<m_name><b>(pfm| init)
           | ~list_vt_cons(x, xs1) =>
               monad_bind<m_name><b, b>
               ( pfm
               | foldM_list_vt$fopr<a, b, m(b)>(x, init)
               , llam(res) => foldM_list_vt$aux<m_name><a, b>{m}{n-1}
                              (pfm| xs1, res) )

        
         fun{m_name: type}{a, b: vt0ype}

         foldM_list_vt_cloref

         {m: fvtype}
         {n: int}
         ( pfm: MONAD(m_name, m)

         | xs: list_vt(a, n)
         , init: b
         , fopr: (a, b) -<cloref1> m(b) ):
         m(b) =
           let implement(a, b, s)
               foldM_list_vt$fopr<a, b, s>(x, init) =

                 let val x = $UN.castvwtp0(x)

                     val init = $UN.castvwtp0(init)
                 in $UN.castvwtp0(fopr(x, init)) end
           in foldM_list_vt$aux<m_name><a, b>{m}{n}(pfm| xs, init) end

         fun{m_name: type}{a, b: vt0ype}

         foldM_list_vt_cloptr

         {m: fvtype}
         {n: int}
         ( pfm: MONAD(m_name, m)

         | xs: list_vt(a, n)
         , init: b
         , fopr: !(a, b) -<lincloptr1> m(b) ):  // Note, [fopr] is not freed!
         m(b) =
           let val foo = $UN.castvwtp1{(a, b) -<cloref1> m(b)}(fopr)
           in foldM_list_vt_cloref<m_name><a, b>{m}{n}(pfm| xs, init, foo) end

Some code to test:

             val zs = $list_vt{int}(7, 8, 9)
        
             val bar =
               llam(z: int, i: int): Option_vt(int) =<cloptr1> return(pfoptm| z + i)

             val- ~Some_vt(z) = foldM_list_vt_cloptr(pfoptm| zs, 0, bar)

It all typechecks but the compiler says

linear_monads_dats.c:5703:1: warning: implicit declaration of function ‘ATSPMVenv’ [-Wimplicit-function-declaration]
 ATSINSmove(tmpret33__1, foldM_list_vt__aux_15__15__1(ATSPMVenv(fopr), env0, arg0)) ;
 ^
In file included from linear_monads_dats.c:15:0:
linear_monads_dats.c:5703:64: error: ‘fopr’ undeclared (first use in this function)
 ATSINSmove(tmpret33__1, foldM_list_vt__aux_15__15__1(ATSPMVenv(fopr), env0, arg0)) ;

If I'm reading this correctly, then it is the same problem all over again. Why does the unsafe casting not work this time around?

[gmhwxi]

The issue you encountered this time is very different.

Your code should compile if you change the body of foldM_list_vt_cloref
as follows (by adding the line 'val () = $tempenver(fopr)"):

             let
             val () = $tempenver(fopr)

             implement(a, b, s)
                 foldM_list_vt$fopr<a, b, s>(x, init) =
                   let val x = $UN.castvwtp0(x)
                       val init = $UN.castvwtp0(init)
                   in $UN.castvwtp0(fopr(x, init)) end
             in foldM_list_vt$aux<m_name><a, b>{m}{n}(pfm| xs, init) end

The use of $tempenver forces the compiler to push 'fopr' into the closure
generated from compiling foldM_list_vt. The compiler does this automatically
most of the time but the programmer may have to use $tempenver occasionally
as the underlying algorithm I used is not complete (but more efficient for handling
most cases).

[August Alm]

Thanks! Th error message is clear to me now. Thank you for the explanation, I will make sure to add $tempenvr to my bag of tricks.

[August Alm]

I've added a bunch of general monadic functions but now I came to a halt. I am now trying to find a good
way to implement "submonad-typeclasses", like state monads. My first attempt was:

         vtypedef
         state(s: vt0ype)(a: vt0ype) = s -<lincloptr1> (a, s)

Then having a state monad is handled by the [prop] [MONAD(m_name, state s)]. That is to say, for general
monads the function templates all had the form

        fun{m_name: type}{...}
        function
        {m: fvtype}
        (pfm: MONAD(m_name, m) | .....

For state monads I want the [m] to be fixed to be of the form [state s] for some [s], and, e.g., write things like

         fun{m_name: type}
         state_modify
         {s: vt0ype}
         (pfm: MONAD(m_name, state s)| fopr: hom(s, s)):
         (state s)(void) =
           llam(st) => let val st = fopr(st)
                            in freehom(fopr); ((), st) end


However, I can't get this to work. The above function [state_modify] will not pass typechecking. Strangely, the compiler
believer the types [s] and [void] are reversed! It cannot infer that [st: s], and instead infers that [st: void]. A function like

         fun{m_name: type}{a: vt0ype}
         state_action
         {s: vt0ype}
         ( pfm: MONAD(m_name, state s)
         | act: s -<lincloptr1> (a, s) ):
         state s (a) =
           llam(st) => let val (x, st') = act(st)
                            in freehom(act); (x, st') end

will also not compile, again because type [a] is inferred as type [s] and vice versa. Simply
switching their names doesn't help though, which leads me to suspect this kind of approach
is fundamentally flawed.

I know I could get it to work with a fixed but abstract type [s] but I would really like to avoid
this route if possible.

I also tried to replace [MONAD(m_name, state s)] with a prop of the form

         STATE(m_name, m, s) =
             ( MONAD(m_name, m)
             , {a: vt0ype} EQ_vt0ype(m(a), state(s, a)) )

that is to say, still keeping the [m: fvtype] but requiring a proof that [m(a)] is really equal to
 
        s -<lincloptr1> (a, s)                          

but I couldn't get this to work either. (Maybe it does work, but I couldn't figure out how.)

How would you do it, professor? :)

Almost all "(co)monad families", e.g. the continuation monad, are of a similar form in that
the constructor [m: fvtype] is restricted to be of a special form depending on a [s: vt0ype],
so if I could just get the state example down then I think all the others would follow easily.

Best wishes,
August

[gmhwxi]

What you reported sounds like a bug in the ATS compiler.
Could you make your code accessible for me to take a look?

Thanks!

[gmhwxi]

 
  It is a bug! I will fix it later. For the moment, you can
  write:

  stadef
  state(s: vt0ype) = lam(a: vt0ype) => s -<lincloptr1> (a, s)

[gmhwxi]

It is a minor fix. The changes uploaded.

[August Alm]

Great you caught it! Now I almost feel useful.

The following will not compile though it passes typechecking:

         fun{}
         state_put
         {s: vt0ype}
         (pfm: MONAD(state_s, state s)| st: s):
         state s (void) =
           llam(_) => ((), st)

The error message says "variable or field declared zero". When
searching for documentation I understand that this is down to how
C/gcc handles [void]. Is there a work around?

[gmhwxi]

You could use 'unit' instead of 'void': unit(): unit

[August Alm]

Thank you, that worked like a charm!

I have now encountered a compiler error I have not seen before.
See https://glot.io/snippets/eoni90xpb9 for self-contained code
that generates it. The error is
 
  "...declared as function returning an array"

I know that a C-function cannot return an array. What I can't figure
out is what in my ATS code that the compiler interprets as a
function returning an array. By the way, the error is spawned by
calling the "bind" for the continuation monad in the main function;
without doing that the code compiles.

Best wishes,
August

[Hongwei Xi]

This issue can be fixed if you change r:vt0ype to r:vtype

in the following definition:

stadef
cont(r: vt0ype) = lam(a: vt0ype) => hom(a, r) -<lincloptr1> r

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/6c0cbf59-8f02-45a6-8cd0-2dd677b85749%40googlegroups.com.

[August Alm]

Hmm. Did I make something that is inherently erroneous (judged wrong from "within" ATS)
or did I run into a peculiarity of gcc?

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/6c0cbf59-8f02-45a6-8cd0-2dd677b85749%40googlegroups.com.

[Hongwei Xi]

If you use t0ype, the compiler cannot figure out the size of r, causing a compilation error.

Sent from my T-Mobile 4G LTE device

------ Original message------

From: August Alm

Date: Wed, Apr 5, 2017 3:18 PM

To: ats-lang-users;

Subject:Re: Template-based implementation for functors

           let val foo = $UN.castvwtp1{(a, b) - m(b)}(fopr)

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/7ad7c8f3-894d-490a-9680-a6254d6ebdce%40googlegroups.com.

[Steinway Wu]

Hi Hongwei and August, 

https://glot.io/snippets/f0nd233vde

I have this functor code working without any "name" hack. @Hongwei, did you make any improvements on templates to make it happen? Or am I missing something? And btw, glot.io is still running ATS 0.2.11. 

[Hongwei Xi]

This approach can only handle simple type constructors like list and maybe.

It would not handle List defined as follows:

typedef List(a:t@ype) = [n:nat] List(a, n)

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/56284850-c51f-4474-b5ae-445e93960a53%40googlegroups.com.

[Steinway Wu]

Oh I see. But anyway, here's a monad type class. Just for the record. 

https://glot.io/snippets/f0nejek645

[Steinway Wu]

I actually just tried it, and it works with `[n:nat] List (a, n)`. See https://glot.io/snippets/f0nf39m7lk. Could you explain a bit more about why it should not work? Is it related to static dispatching, like checking type equalities and choosing which template to use? 

[gmhwxi]

I am a bit surprised. It did not work. It works now because of a recent
change I made on checking type equality (my guess).