class Functor < Type -> Type

{vars f : Functor; a, b, c : Type

op map : (a -> b) -> f a -> f b

vars x : f a; f : a -> b; g : b -> c

. (map \ y : a .! y) x = x

. (map \ y : a .! g (f y)) x = map g (map f x);

}

class Monad < Type -> Type

{vars m : Monad; a, b, c : Type

ops __>>=__ : m a * (a ->? m b) ->? m b;

__>>=__ : m a * (a -> m b) -> m b;

ret : a -> m a

vars x, y : a; p : m a; q : a ->? m b; r : b ->? m c; f : a ->? b

. def q x => ret x >>= q = q x

. (p >>= \ x : a . ret (f x) >>= r) = p >>= \ x : a . r (f x)

. p >>= ret = p

. (p >>= q) >>= r = p >>= \ x : a . q x >>= r

. (ret x : m a) = ret y => x = y;

}

class instance Monad < Functor

vars m : Monad; a, b : Type; f : a -> b; x : m a

. map f x = x >>= \ y : a . ret (f y);

class MonadT < Monad -> Monad

{vars t : MonadT; m : Monad; a : Type

op lift : m a -> t m a

vars x : a; p : m a; b : Type; q : a -> m b

. lift (ret x) = (ret x : t m a)

. lift (p >>= q) = lift p >>= \ y : a .! lift (q y) : t m b;

}

var state : Type

type instance ST state : Monad

vars a, b : Type

type ST state a := state ->? a * state

vars x : a; p : ST state a; q : a ->? ST state b

classes

Functor : Type -> Type;

Monad : Type -> Type;

MonadT : (Type -> Type) -> Type -> Type

classes

Monad < Functor;

MonadT < Monad -> Monad

types

ST : Type -> Monad;

gn_t1030 : Type -> Type

types

ST := \ state : Type . gn_t1030;

gn_t1030 := \ a : Type . state ->? a * state

vars

a : Type %(var_1026)%;

b : Type %(var_1027)%;

c : Type %(var_85)%;

f : Functor %(var_1)%;

m : Monad %(var_752)%;

state : Type %(var_1024)%;

t : MonadT %(var_751)%

op __>>=__ : forall m : Monad; a : Type; b : Type

. m a * (a -> m b) -> m b

%(op)%

op __>>=__ : forall m : Monad; a : Type; b : Type

. m a * (a ->? m b) ->? m b

%(op)%

op lift : forall t : MonadT; m : Monad; a : Type . m a -> t m a

%(op)%

op map : forall f : Functor; a : Type; b : Type

. (a -> b) -> f a -> f b

%(op)%

op ret : forall m : Monad; a : Type . a -> m a %(op)%

vars

f : a -> b;

g : b -> c;

p : ST state a;

q : a ->? ST state b;

r : b ->? m c;

x : a;

y : a

forall a : Type; f : Functor; x : f a . (map \ y : a .! y) x = x

forall

a : Type; b : Type; c : Type; f : Functor; f : a -> b; g : b -> c;

x : f a

. (map \ y : a .! g (f y)) x = map g (map f x)

forall a : Type; b : Type; m : Monad; q : a ->? m b; x : a

. def q x => (__>>=__ : m a * (a ->? m b) ->? m b) (ret x, q) = q x

forall

a : Type; b : Type; c : Type; m : Monad; f : a ->? b; p : m a;

r : b ->? m c

. (__>>=__ : m a * (a ->? m c) ->? m c)

(p, \ x : a . (__>>=__ : m b * (b ->? m c) ->? m c) (ret (f x), r))

= (__>>=__ : m a * (a ->? m c) ->? m c) (p, \ x : a . r (f x))

forall a : Type; m : Monad; p : m a

. (__>>=__ : m a * (a ->? m a) ->? m a) (p, ret) = p

forall

a : Type; b : Type; c : Type; m : Monad; p : m a; q : a ->? m b;

r : b ->? m c

. (__>>=__ : m b * (b ->? m c) ->? m c)

((__>>=__ : m a * (a ->? m b) ->? m b) (p, q), r)

= (__>>=__ : m a * (a ->? m c) ->? m c)

(p, \ x : a . (__>>=__ : m b * (b ->? m c) ->? m c) (q x, r))

forall a : Type; m : Monad; x : a; y : a

. (ret x : m a) = ret y => x = y

forall a : Type; b : Type; m : Monad; f : a -> b; x : m a

. map f x

= (__>>=__ : m a * (a ->? m b) ->? m b) (x, \ y : a . ret (f y))

forall a : Type; m : Monad; t : MonadT; x : a

. lift (ret x) = (ret x : t m a)

forall

a : Type; b : Type; m : Monad; t : MonadT; p : m a; q : a -> m b

. lift ((__>>=__ : m a * (a ->? m b) ->? m b) (p, q))

= (__>>=__ : t m a * (a ->? t m b) ->? t m b)

(lift p, \ y : a .! lift (q y) : t m b)

### Hint 2.7, is type variable 'f'

### Hint 2.19, is type variable 'a'

### Hint 2.22, is type variable 'b'

### Hint 2.25, is type variable 'c'

### Hint 4.8, not a kind 'f a'

### Hint 4.16, not a class 'a'

### Hint 4.16, not a class 'b'

### Hint 4.27, not a class 'b'

### Hint 4.27, not a class 'c'

### Hint 9.7, is type variable 'm'

### Hint 9.17, is type variable 'a'

### Hint 9.17, rebound type variable 'a'

### Hint 9.20, is type variable 'b'

### Hint 9.20, rebound type variable 'b'

### Hint 9.23, is type variable 'c'

### Hint 9.23, rebound type variable 'c'

### Hint 13.8, not a class 'a'

### Hint 13.7, rebound variable 'x'

### Hint 13.11, not a class 'a'

### Hint 13.17, not a kind 'm a'

### Hint 13.25, not a kind 'a ->? m b'

### Hint 13.39, not a kind 'b ->? m c'

### Hint 13.53, not a kind 'a ->? b'

### Hint 13.52, rebound variable 'f'

### Hint 14.14-14.24, rejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a) (var x : a),

(var q : a ->? m b))'

### Hint 14.14-14.24, untypable term (with type: _v106_m _v107_a * (_v107_a -> _v106_m _v108_b))

'(ret x, q)'

### Hint 15.12, rebound variable 'x'

### Hint 15.19-15.33, rejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a)

((var f : a ->? b) (var x : a)),

(var r : b ->? m c))'

### Hint 15.19-15.33, untypable term (with type: _v203_m _v204_a * (_v204_a -> _v203_m _v205_b))

'(ret (f x), r)'

### Hint 15.3-15.33, rejected '__->?__ < __->__' of '((var p : m a),

\ x : a

. (op __>>=__ :

forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)

((op ret : forall m : Monad; a : Type . a -> m a)

((var f : a ->? b) (var x : a)),

(var r : b ->? m c)))'

### Hint 15.3-15.26, untypable term (with type: _v166_m _v167_a * (_v167_a -> _v166_m _v168_b))

'(p, \ x : a . ret (f x) >>= r)'

### Hint 15.12, rebound variable 'x'

### Hint 15.19-15.33, rejected '__->?__ < __->__' of '((op ret : forall m : Monad; a : Type . a -> m a)

((var f : a ->? b) (var x : a)),

(var r : b ->? m c))'

### Hint 15.19-15.33, untypable term (with type: _v254_m _v255_a * (_v255_a -> _v254_m _v256_b))

'(ret (f x), r)'

### Hint 16.13, rebound variable 'x'

### Hint 16.5-16.25, rejected '__->?__ < __->__' of '((var p : m a),

\ x : a . (var r : b ->? m c) ((var f : a ->? b) (var x : a)))'

### Hint 16.5-16.25, untypable term (with type: _v304_m _v305_a * (_v305_a -> _v304_m _v306_b))

'(p, \ x : a . r (f x))'

### Hint 16.13, rebound variable 'x'

### Hint 18.4-18.10, rejected '__->?__ < __->__' of '((var p : m a), (var q : a ->? m b))'

### Hint 18.4-18.10, untypable term (with type: _v446_m _v447_a * (_v447_a -> _v446_m _v448_b))

'(p, q)'

### Hint 18.3-18.17, rejected '__->?__ < __->__' of '((op __>>=__ :

forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)

((var p : m a), (var q : a ->? m b)),

(var r : b ->? m c))'

### Hint 18.3-18.17, untypable term (with type: _v410_m _v411_a * (_v411_a -> _v410_m _v412_b))

'(p >>= q, r)'

### Hint 18.4-18.10, rejected '__->?__ < __->__' of '((var p : m a), (var q : a ->? m b))'

### Hint 18.4-18.10, untypable term (with type: _v482_m _v483_a * (_v483_a -> _v482_m _v484_b))

'(p, q)'

### Hint 18.29, rebound variable 'x'

### Hint 18.36-18.44, rejected '__->?__ < __->__' of '((var q : a ->? m b) (var x : a), (var r : b ->? m c))'

### Hint 18.36-18.44, untypable term (with type: _v555_m _v556_a * (_v556_a -> _v555_m _v557_b))

'(q x, r)'

### Hint 18.21-18.44, rejected '__->?__ < __->__' of '((var p : m a),

\ x : a

. (op __>>=__ :

forall m : Monad; a : Type; b : Type . m a * (a ->? m b) ->? m b)

((var q : a ->? m b) (var x : a), (var r : b ->? m c)))'

### Hint 18.21-18.36, untypable term (with type: _v518_m _v519_a * (_v519_a -> _v518_m _v520_b))

'(p, \ x : a . q x >>= r)'

### Hint 18.29, rebound variable 'x'

### Hint 18.36-18.44, rejected '__->?__ < __->__' of '((var q : a ->? m b) (var x : a), (var r : b ->? m c))'

### Hint 18.36-18.44, untypable term (with type: _v600_m _v601_a * (_v601_a -> _v600_m _v602_b))

'(q x, r)'

### Hint 20.16, refined class 'Monad'

### Hint 21.7, is type variable 'm'

### Hint 21.7, rebound type variable 'm'

### Hint 21.17, is type variable 'a'

### Hint 21.17, rebound type variable 'a'

### Hint 21.20, is type variable 'b'

### Hint 21.20, rebound type variable 'b'

### Hint 21.30, not a class 'a'

### Hint 21.30, not a class 'b'

### Hint 21.29, rebound variable 'f'

### Hint 21.41, not a kind 'm a'

### Hint 21.40, rebound variable 'x'

### Hint 22.21, rebound variable 'y'

### Hint 22.13-22.35, rejected '__->?__ < __->__' of '((var x : m a),

\ y : a

. (op ret : forall m : Monad; a : Type . a -> m a)

((var f : a -> b) (var y : a)))'

### Hint 22.13-22.35, untypable term (with type: _v699_m _v700_a * (_v700_a -> _v699_m _v701_b))

'(x, \ y : a . ret (f y))'

### Hint 22.21, rebound variable 'y'

### Hint 25.7, is type variable 't'

### Hint 25.18, is type variable 'm'

### Hint 25.18, rebound type variable 'm'

### Hint 25.28, is type variable 'a'

### Hint 25.28, rebound type variable 'a'

### Hint 27.8, not a class 'a'

### Hint 27.7, rebound variable 'x'

### Hint 27.14, not a kind 'm a'

### Hint 27.13, rebound variable 'p'

### Hint 27.21, is type variable 'b'

### Hint 27.21, rebound type variable 'b'

### Hint 27.31, not a kind 'a -> m b'

### Hint 27.30, rebound variable 'q'

### Hint 29.33, rebound variable 'y'

### Hint 29.33, rebound variable 'y'

### Hint 29.33, rebound variable 'y'

### Hint 29.33, rebound variable 'y'

### Hint 31.7, is type variable 'state'

### Hint 33.7, is type variable 'a'

### Hint 33.7, rebound type variable 'a'

### Hint 33.10, is type variable 'b'

### Hint 33.10, rebound type variable 'b'

### Hint 34.6, redeclared type 'ST'

### Hint 35.8, not a class 'a'

### Hint 35.7, rebound variable 'x'

### Hint 35.14, not a kind 'ST state a'

### Hint 35.13, rebound variable 'p'

### Hint 35.29, not a kind 'a ->? ST state b'

### Hint 35.28, rebound variable 'q'

### Hint 36.7, in type of '(var x : a)'

typename 'a' (35.10)

is not unifiable with type 'a * state' (36.20)

### Hint 36.7, untypable term (with type: a * state)

'x'

### Hint 36.3-36.42, untypable term (with type: ? _v1033_a * ? _v1033_a)

'(ret x : ST state a, \ s : state . (x, s))'

*** Error 36.3, no typing for '(ret x : ST state a) = \ s : state . (x, s)'

### Hint 37.3-37.9, in type of '((var p : ST state a), (var q : a ->? ST state b))'

typename 'a' (35.31)

is not unifiable with type 'a * state' (35.25)

### Hint 37.3-37.9, untypable term (with type: _v1058_m _v1059_a * (_v1059_a -> _v1058_m _v1060_b))

'(p, q)'

### Hint 37.3-37.9, in type of '((var p : ST state a), (var q : a ->? ST state b))'

typename 'a' (35.31)

is not unifiable with type 'a * state' (35.25)

### Hint 37.3-37.9, untypable term (with type: _v1061_m _v1062_a * (_v1062_a ->? _v1061_m _v1063_b))

'(p, q)'

### Hint 37.5-37.54, untypable term (with type: ? _v1051_a * ? _v1051_a)

'(p >>= q, \ s1 : state . let (z, s2) = p s1 in q z s2)'

*** Error 37.5, no typing for 'p >>= q = \ s1 : state . let (z, s2) = p s1 in q z s2'