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

ops __comp__ : (b -> c) * (a -> b) -> a -> c;

id : a -> a

. id x = x

. (g comp f) x = g (f x);

class Functor < Type -> Type

{vars a, b, c : Type; F : Functor; f : a -> b; g : b -> c

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

. map id = (id : F a -> F a)

. (map (g comp f) : F a -> F c) = map g comp map f;

}

class PolyFunctor < Functor

class PolyBifunctor < Type -> PolyFunctor

vars F : Functor; a, b : Type

type Alg F a := F a -> a

op __::__->__ : Pred ((a -> b) * (Alg F a) * (Alg F b))

class DTFunctor < Functor

{vars F : DTFunctor; a : Type

type InitialCarrier F

ops initialAlg : Alg F (InitialCarrier F);

fold : Alg F a -> InitialCarrier F -> a

vars alpha : Alg F a; g : InitialCarrier F -> a

. g :: initialAlg -> alpha <=> g = fold alpha;

}

class PolyFunctor < DTFunctor

var G : PolyBifunctor

type ParamDT G a := InitialCarrier (G a)

type ParamDT G : DTFunctor

vars l : ParamDT G a; f : a -> a

classes

DTFunctor < Type -> Type;

Functor < Type -> Type;

PolyBifunctor < Type -> Type -> Type;

PolyFunctor < Type -> Type

classes

DTFunctor < Functor;

PolyBifunctor < Type -> PolyFunctor;

PolyFunctor < DTFunctor

types

Alg : Functor -> Type -> Type;

InitialCarrier : DTFunctor -> Type;

ParamDT : PolyBifunctor -> DTFunctor

types

Alg (F : Functor) (a : Type) := F a -> a;

ParamDT (G : PolyBifunctor) (a : Type) := InitialCarrier (G a)

vars

F : DTFunctor %(var_59)%;

G : PolyBifunctor %(var_75)%;

a : Type %(var_60)%;

b : Type %(var_56)%;

c : Type %(var_12)%

op __::__->__ : forall F : Functor; a : Type; b : Type

. Pred ((a -> b) * Alg F a * Alg F b)

op __comp__ : forall a : Type; b : Type; c : Type

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

op fold : forall F : DTFunctor; a : Type

. Alg F a -> InitialCarrier F -> a

op id : forall a : Type . a -> a

op initialAlg : forall F : DTFunctor . Alg F (InitialCarrier F)

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

. (a -> b) -> F a -> F b

vars

alpha : Alg F a;

f : a -> a;

g : InitialCarrier F -> a;

l : ParamDT G a;

x : a

forall a : Type; x : a . id x = x

forall a : Type; b : Type; c : Type; f : a -> b; g : b -> c; x : a

. (g comp f) x = g (f x)

forall F : Functor; a : Type . map id = (id : F a -> F a)

forall

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

. (map (g comp f) : F a -> F c) = map g comp map f

forall

F : DTFunctor; a : Type; alpha : Alg F a; g : InitialCarrier F -> a

. g :: initialAlg -> alpha <=> g = fold alpha

1.6: ### Hint: is type variable 'a'

1.8: ### Hint: is type variable 'b'

1.10: ### Hint: is type variable 'c'

1.20: ### Hint: not a class 'a'

1.26: ### Hint: not a class 'a'

1.26: ### Hint: not a class 'b'

1.37: ### Hint: not a class 'b'

1.37: ### Hint: not a class 'c'

2.18-2.23: ### Hint:

no kind found for 'b -> c'

expected: {Cpo}

found: {Type}

2.18-2.23: ### Hint:

no kind found for 'b -> c'

expected: {Cppo}

found: {Type}

8.7: ### Hint: is type variable 'a'

8.7: ### Hint: rebound type variable 'a'

8.9: ### Hint: is type variable 'b'

8.9: ### Hint: rebound type variable 'b'

8.11: ### Hint: is type variable 'c'

8.11: ### Hint: rebound type variable 'c'

8.20: ### Hint: is type variable 'F'

8.33: ### Hint: not a class 'a'

8.33: ### Hint: not a class 'b'

8.32: ### Hint: rebound variable 'f'

8.44: ### Hint: not a class 'b'

8.44: ### Hint: not a class 'c'

8.43: ### Hint: rebound variable 'g'

16.5: ### Hint: is type variable 'F'

16.5: ### Hint: rebound type variable 'F'

16.17: ### Hint: is type variable 'a'

16.17: ### Hint: rebound type variable 'a'

16.19: ### Hint: is type variable 'b'

16.19: ### Hint: rebound type variable 'b'

18.23-18.28: ### Hint:

no kind found for 'a -> b'

expected: {Cpo}

found: {Type}

18.23-18.28: ### Hint:

no kind found for 'a -> b'

expected: {Cppo}

found: {Type}

21.5: ### Hint: is type variable 'F'

21.5: ### Hint: rebound type variable 'F'

21.19: ### Hint: is type variable 'a'

21.19: ### Hint: rebound type variable 'a'

25.10: ### Hint: not a kind 'Alg F a'

25.22: ### Hint: not a kind 'InitialCarrier F -> a'

25.21: ### Hint: rebound variable 'g'

28.7-28.17: ### Warning: refined class 'PolyFunctor'

29.5: ### Hint: is type variable 'G'

33.7: ### Hint: not a kind 'ParamDT G a'

33.23: ### Hint: not a class 'a'

33.23: ### Hint: not a class 'a'

33.22: ### Hint: rebound variable 'f'

34.9: ### Hint:

in type of '(var l : ParamDT G a)'

type 'InitialCarrier' (30.34)

is not unifiable with differently kinded type '_v82_F' (9.21)

34.9: ### Hint: untypeable term (with type: _v82_F _v80_a) 'l'

34.3-34.29: ### Hint:

untypeable term (with type: ? _v79_a * ? _v79_a)

'(map f l, fold initialAlg l)'

34.11: *** Error: no typing for 'map f l = fold initialAlg l'