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