[Ur] 'Anonymous function remains' in state monad

[Sergey Mironov]

I don't get the idea this time, actually, functors and signatures is
still a less-known area for me.  Could you please explain it in more
details?

Still there is something that worrying me when it comes to functors. I
may guess, that moving [monad_state] to the signature would require
[state] to be defined in signature as well; we would get something
like the following (sorry for the possible mistakes)

functor Trans(S :
sig
  con m :: Type -> Type

  val monad_m : monad m

  con st :: Type

  con state :: a :: Type -> st -> a -> S.m (st * a)

  val monad_state : monad (state st)

end) :

...

This design has serious side effect: user would have to explicitly
define the [st] (a state of our state monad) in order to instantiate
the functor. Next, I know that, according to Ur/Web syntax, we are
allowed to define functors in global space only. Now, the problem is
we often don't know the exact value of [st] in global space. For
example, the [nest] combinator is defined in XmlGen.ur as

fun nest [a ::: Type] [ctx:::{Unit}] [ctx2 :::{Unit}]
    (f:xml ctx2 [] [] -> xml ctx [] [])
    (x:MT.state (xml ctx2 [] []) a)
      : MT.state (xml ctx [] []) a =
  (xml2,a) <- MT.lift (MT.run <xml/> x);
  push (f xml2);
  return a

It does a 'junction' from [state (xml ctx2 [] [])] to [state (xml ctx
[] [])] by applying function [f]. We are allowed to refer to [ctx] and
[ctx2] only inside nest's body, but we can't define new State.Trans
functor there! That's why I would like to keep [st]'s definition as
is, on a function level and not to move it to the functor's signature.

Regards,
Sergey



2014-08-16 1:58 GMT+04:00 Adam Chlipala <adamc at csail.mit.edu>:
> In my modification of your starting code, I made the type family
> [monad_state] abstract in the module signature, instead of giving its
> definition.  Everything works fine in that case, and I think it's nicer from
> a modularity perspective.
>
>
> On 08/15/2014 02:46 PM, Sergey Mironov wrote:
>>
>> OK, I understand the idea. Unfortunately, compiler seems to go crazy
>> after this change. The first error message is following:
>>
>> urweb -dbms sqlite ./test/Test4
>> /home/grwlf/proj/urweb-monad-pack/test/Test4.ur:10:11: (to 10:20)
>> Unification failure
>> Expression:  MO.get [<UNIF:U11::Type>] {}
>>    Have con:
>> <UNIF:U11::Type>  ->  option (<UNIF:U11::Type>  *<UNIF:U11::Type>)
>>    Need con:<UNIF:U8::Type ->  Type>  <UNIF:U9::Type>
>>
>> Looks like it doesn't want to use the monad_state instance as aid for
>> code generation or something like that..
>> I've pushed the changes to the github.
>>
>
>
>
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur