Free Semigroup and Monoid types

[AshleyYakeley]

datatype Semigroup +a = MkSemigroup (List1 a)
datatype Monoid +a = MkMonoid (List a)
(++): a -> a -> Semigroup a
single: a -> Semigroup a
empty: Monoid None
concat1: List1 a -> Monoid a
concat: List a -> Monoid a
Semigroup (List1 a) <: List1 a
Monoid (List a) <: List a
Semigroup a <: Monoid a
Monoid Text <: Text

[AshleyYakeley]

Problem: there's a diamond:

1. Semigroup _ <: Monoid _ <: List _
2. Semigroup _ <: List1 _ <: List _

Rules are: Semigroup a <: Monoid a Monoid (List a) <: List a Semigroup (List1 a) <: List1 a List1 a <: List a

Given Semigroup (List Unit) <: List Unit, we get

1. Semigroup (List Unit) <: Monoid a and Monoid a <: List Unit (OK)
2. Semigroup (List Unit) <: List1 a and List1 a <: List Unit (first one fails)

[AshleyYakeley]

Solution might just be to try all in the diamond.

[AshleyYakeley]

This is causing problems:

1. Consider f = \x => [()] ++ x Inferred: f: a -> Semigroup (a | List1 Unit) Cannot subsume to List Unit -> List Unit.

2. Simplify List1 Unit|List Unit Result: hangs

[AshleyYakeley]

Can we join the conversions?

F A -> G C
F B -> G D

This depends on the polarities.

• F (A | B) -> G (C | D) can be constructed
• F (A & B) -> G (C & D) can be constructed
• F (A & B) -> G (C | D) can be constructed but is less useful than either one
• F (A | B) -> G (C & D) cannot be constructed

[AshleyYakeley]

Also have this diamond:

1. Monoid _ <: Text <: Literal <: Entity
2. Monoid _ <: List _ <: Entity

Rules are: Monoid Text <: Text List Entity <: Entity Monoid (List a) <: List a

This gives: Monoid Text <: Entity Monoid (List Entity) <: Entity

Consider:

p: a -> Monoid a
q: Entity -> Entity
r = fn x => q (p x)

What is the type of r? Either

1. Text -> Entity
2. List Entity -> Entity

These cannot be joined.

UPDATE: in this case, Pinafore would reject r for incoherent ground type conversions.

[AshleyYakeley]

Can't be done.

[AshleyYakeley]

This is possible actually.

[AshleyYakeley]

Consider:

Monoid Text <: Entity
Monoid (List Entity) <: Entity

p: a -> Monoid a
q: Entity -> Entity
r1 = fn x => q (p x)
r2 = fn x => q (p (x: Text))

Pinafore rejects r1 but accepts r2. Is this OK?

[AshleyYakeley]

No, because we have Monoid Text <: Text and Text <: Entity, but not Monoid Text <: Entity, violating the composition rule.

Monoid Text <: Entity exists only as a (composed) subtype conversion entry, not as an actual subtype relation.

[AshleyYakeley]

Nope.