[Ur] Poor inference of monads over "non-canonical" types

[Evan Danaher]

Thanks for the quick reply!

As usual, the answer is obvious in hindsight: the issue is with
"non-canonical" types, so make in canonical by wrapping it in a
constructor.  There can be ambiguity if there are multiple matches;
avoid that by wrapping it in a (unique) constructor.

On the upside, in fighting this, I'm getting much more comfortable with
the type system on an intuitive level, which is definitely valuable.

On Sat, Feb 22, 2014 at 12:12:16AM -0500, Patrick Hurst wrote:
> Your code is equivalent to this in Haskell:
> 
>     type Pair a = (a, a)
> 
>     instance Monad Pair where
>         return = undefined
>         (>>=) = undefined
> 
> which is illegal. The Haskell way to do it would be:
> 
>     data Pair' a = MkPair (a, a)
> 
>     instance Monad Pair' where
>         return = undefined
>         (>>=) = undefined
> 
> The difference is that [(2, 3) :: Pair Int] is valid, but [(2, 3) ::
> Pair' Int] isn't; you need to apply [MkPair :: (a, a) -> Pair' a] to get
> [MkPair (2, 3) :: Pair' Int].
> 
> The Ur/Web equivalent of this would be
> 
>     datatype pair a = Pair of a * a
>     val pairMonad : monad pair = mkMonad {
>       Return = fn [t ::: Type] (a : t) => Pair (a, a),
>       Bind = fn [t1 ::: Type] [t2 ::: Type] ((Pair (a, a')) : pair t1) (b : t1 -> pair t2) => b a
>     }
> 
>     val fail : pair int =
>          return 4
> 
> which does work.
> 
> 
> Evan Danaher <ur at edanaher.net> writes:
> 
> > I'm writing a simple parser, and decided to try my hand at a
> > Parsec-like monadic combinator approach.  Unfortunately, it seems that
> > monad inference is fairly weak; consider the following:
> >
> >   con pair t = t * t
> >   val pairMonad : monad pair = mkMonad {
> >     Return = fn [t ::: Type] (a : t) => (a, a),
> >     Bind = fn [t1 ::: Type] [t2 ::: Type] ((a, a') : pair t1) (b : t1 -> pair t2) => b a
> >   }
> >
> >   val fail : pair int =
> >     return 4
> >
> > (Yes, that's not actually a monad, but the types work.)  This fails to compile:
> >
> >   Expression:  return [<UNIF:U338::Type -> Type>] [int] _ 4
> >     Have con:  <UNIF:U338::Type -> Type> int
> >     Need con:  int * int
> >   Incompatible constructors
> >   Have:  <UNIF:U338::Type -> Type> int
> >   Need:  int * int
> >
> > It looks like the compiler is simplifying (pair int) to (int * int), then
> > failing to unify it with the (M t) pattern to pull out the monad.  Sure enough:
> >
> >   val fail : pair int =
> >     @return pairMonad 4
> >
> > works just fine, since pairMonad provides the monad, and then unifying (t * t)
> > with (int * int) doesn't cause any trouble.
> >
> > I can see why this could be tricky, and in general possibly ambiguous.  (E.g.,
> > if there's a second monad (con withInt t = t * int), int * int could be either
> > of them.)  However, I'd expect it to be reasonable to take the given type (pair
> > int) and use that one.  (How does Haskell handle this?)
> >
> > Moreover, this (AFAICT) completely breaks the syntactic sugar for monads; I'd
> > like to be able to write something like
> >   
> >   command <- Parse.word;
> >   args <- Parse.arguments;
> >   return {Command=command, Args=args}
> >
> > but the suger doesn't seem to provide any way to annotate the monad, rendering
> > it uncompilable.
> >
> > Hopefully the problem is clear; am I missing an obvious solution?  I can't find
> > anything in the bug tracker about this; I can't imagine I'm the first to run
> > into it.
> >
> > _______________________________________________
> > Ur mailing list
> > Ur at impredicative.com
> > http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>