Murat Kasimov

More about me

Я language (β)

/Я language (β)/Tutorials/Wolf, goat and cabbage solver 1/

Full source codeNext chapter

A farmer with a wolf, a goat, and a cabbage must cross a river by boat. The boat can carry only the farmer and a single item. If left unattended together, the wolf would eat the goat, or the goat would eat the cabbage. The farmer must help them all cross the river without anything being eaten.

By solving this puzzle we constantly need to choose between items so let's model it with a Sum:

: Thing ~ Unit `S` Unit `S` Unit > Cabbage x = This ( This x ) > Goat x = That ( This x ) > Wolf x = That x

Therefore deconstructing item (knowing which option is there) is essentially factoring through a Sum:

> Cabbage `has` Goat `has` Wolf = identity : Thing `AR` Thing > Cabbage `ho'ut'st` False `has` Goat `ho'ut'st` True `has` Wolf `ho'ut'st` False `har'st` Goat = True Unit > Cabbage `ho'ut'st` False `has` Goat `ho'ut'st` True `has` Wolf `ho'ut'st` False `har'st` Wolf = False Unit

It's possible to express it shorter but then we loose visual tips - it's getting more important if Sum is big like Latin:

> False `has` True `has` False `har'st` Goat = True Unit > False `has` True `has` False `har'st` Wolf = False Unit

If you don't want to deconstruct Sum manually it's possible to use equality relation:

> equals x = Error `ho'ut'st` False `has` Same `ho'ut'st` True `ha_'hjd'eq` x > equals `har'st` Goat `har'st` Wolf = False Unit > equals `har'st` Wolf `har'st` Wolf = True Unit

We can wrap this expression into a logical predicate:

> equals `har'st` Wolf `rya` Enter : Match Thing

The main advantage is that we get a contravariant functor:

> `ya` : a o . Match a `AR_____` a `RA____` o `AR____` Match o

Its parameter positioned contravariantly is effectively its representing object:

> equals `har'st` Wolf `rya` Enter @ Match @ Thing `yar'st` Wolf = True Unit > equals `har'st` Wolf `rya` Enter @ Match @ Thing `yar'st` Goat = False Unit

Another use case of factoring through a Sum is co-representing datastructures:

> Cabbage `ryo` Enter @ List > Cabbage `has` Wolf `ryo` Enter @ List > Cabbage `has` Goat `ryo` Enter @ List

Unlike Match List of any size is a covariant functor:

> `yo` : a o . List _ a `AR_____` a `AR____` o `AR____` List _ o

We need this covariant functor to track content of the river shores between transitions - there are two cases that are considered unacceptable a boat to leave to due to some creatures meal preferences:

> Goat `has` Cabbage `ryo` Enter @ List @ Thing > Wolf `has` Goat `ryo` Enter @ List @ Thing

We already have logical predicates - but they are defined for individual items. Can we somehow make them work for list of items? Yes.

At first sight they seem incompatible - Match is contravariant and List is covariant therefore there is no natural transformation between them... but there is at least one between their compositions! If variances of two functors are not the same - their composition is contravariant.

If we first map over covariantly a lax Kleisli morphism and then apply a component of that natural transformation that swaps functors we get lax Kleisli morphisms at both source and target categories:

There is an operator for such a mappings arrangement:

> `yokl` : a o . List _ a `AR___` a `AR__` Match o `AR__` Match ( List _ o )

Having a list of items, we can turn each of them into a logical predicate that compare another item to original one and then turn a list inside out so that we get a predicate on a list of items:

> Wolf `has` Goat `ryo` Enter `yokl` Forth `ha` Found `ha` Match `ha` equals : Match `T'TT` List `T'I_` Thing

No matter of order this logical predicate is satisfied only if all items listed are found:

> Wolf `has` Goat `ryo` Enter `yokl` Forth `ha` Found `ha` Match `ha` equals `yar_` Wolf `has` Goat `ryo` Enter = True Unit > Wolf `has` Goat `ryo` Enter `yokl` Forth `ha` Found `ha` Match `ha` equals `yar_` Goat `has` Wolf `ryo` Enter = True Unit > Wolf `has` Goat `ryo` Enter `yokl` Forth `ha` Found `ha` Match `ha` equals `yar_` Cabbage `has_` Goat `has` Wolf `ryo` Enter = True Unit > Wolf `has` Goat `ryo` Enter `yokl` Forth `ha` Found `ha` Match `ha` equals `yar_` Wolf `has` Cabbage `ryo` Enter = False Unit > Wolf `has` Goat `ryo` Enter `yokl` Forth `ha` Found `ha` Match `ha` equals `yar_` Goat `ryo` Enter = False Unit

Congratulations, we just designed conditionals upon which we make stateful transitions!

In the next chapter we will focus on State mechanics for finding possible solutions.