AshleyYakeley / Truth

Changes and Pinafore projects. Pull requests not accepted.
https://pinafore.info/
GNU General Public License v2.0
32 stars 0 forks source link

Lens Hierarchy #147

Closed AshleyYakeley closed 1 year ago

AshleyYakeley commented 2 years ago

(Not sure all these are necessary.)

AshleyYakeley commented 1 year ago

Maybe do the rename for 0.4, leave the rest for later.

AshleyYakeley commented 1 year ago

rename is now #179

AshleyYakeley commented 1 year ago

Most general case for mapping WholeModel:

maybeLensMapWholeModel:
  (Maybe aq -> Maybe bq) -> (Maybe bp -> Maybe aq -> Maybe (Maybe ap)) -> WholeModel {-ap,+aq} -> WholeModel {-bp,+bq}

Ignoring the range-variance, that gives:

get: Maybe a -> Maybe b
putback: Maybe b -> Maybe a -> Maybe (Maybe a)

Usual lens has:

get: a -> b
putback: b -> a -> a

Codec has:

decode: a -> Maybe b
encode: b -> a

Reversed codec has:

encode: a -> b
decode: b -> Maybe a
AshleyYakeley commented 1 year ago

What about sums and products? Consider:

a = b +: x
decode: a -> Maybe b
encode: b -> a

a = b *: x
get: a -> b
putback: b -> a -> a

That is, codec for sum, lens for product.

Awkward generalisation:

a = (b *: x) +: y
decode: a -> Maybe b
putback: b -> a -> a
AshleyYakeley commented 1 year ago
type Know = Maybe
type Allow = Maybe

Iso a b
get: a -> b
put: b -> a

Lens a b
get: a -> b
putback: b -> ConstFunction a a

Prism a b -- formerly Codec
getm: a -> Know b
put: b -> a

Conversion a b
getm: a -> Know b
putm: b -> Allow a
inversion: Conversion a b -> Conversion b a

Part a b
getm: a -> Know b
putback: b -> ConstFunction a a

Thing a b
-- null a implies null b
-- setting null b is blocked
getm: a -> Know b
putbackm: b -> ConstFunction (Know a) (Allow a)

Full a b
getmm: Know a -> Know b
putbackmm: Know b -> ConstFunction (Know a) (Allow (Know a))

Iso a b <: Lens a b <: Part a b <: Thing a b <: Full a b
Iso a b <: Prism a b <: Conversion a b <: Thing a b
Prism a b <: Part a b
AshleyYakeley commented 1 year ago

Part doesn't work, because Lens and Prism have incompatible putbacks.

AshleyYakeley commented 1 year ago

I think we want four:

The first three are subtypes of the fourth.

AshleyYakeley commented 1 year ago

done in branch

AshleyYakeley commented 1 year ago

merged