Murat Kasimov

More about me

Я language (β)

/Я language (β)/Behaviour/First/

> First : forall t i . t `C'AR__` t `L` Stops i `T` _

Interpretation: this label point to a first item that does exist.

Demonstration: Arrow component relating to a First item in a List:

> derive `ha` First `har___` Null `ho'vt` Unit `ryo` Enter = Empty `har` Unit > derive `ha` First `har___` Only `ho'ut'st` A `_ryo` Enter = Exist `har'st` A

Demonstration: Scope components relating to a First item in a List:

> this `ha` within `ha` First `har___` Null `ho'vt` Unit `ryo` Enter = Empty `har` Unit > this `ha` within `ha` First `har___` Only `ho'ut'st` B `_ryo` Enter = Exist `har'st` A > that `ha` within `ha` First `har___` Null `ho'vt` Unit `ryo` Enter `har___` Empty `har` Unit = Null `ho'vt` Unit `ryo` Enter > that `ha` within `ha` First `har___` Null `ho'vt` Unit `ryo` Enter `har___` Exist `har'st` A = Null `ho'vt` Unit `ryo` Enter > that `ha` within `ha` First `har___` Only `ho'ut'st` B `_ryo` Enter `har___` Empty `har` Unit = Null `ho'vt` Unit `ryo` Enter > that `ha` within `ha` First `har___` Only `ho'ut'st` B `_ryo` Enter `har___` Exist `har'st` A = Only `ho'ut'st` A `_ryo` Enter

Demonstration: converting a Product of Maybe items into Maybe of Sum of these items:

> Exist `har'st` A `hjd__'ys` First `ha` Exist `har'st` B = Exist `ha` This `har'st` A > Empty `har` Unit `hjd_'ys` First `ha` Exist `har'st` B = Exist `ha` That `har'st` B > Empty `har` Unit `hjd_'ys` First `ha` Empty `har` Unit = Empty `har` Unit > Exist `har'st` A `hjd__'ys` First `ha` Empty `har` Unit = Exist `ha` This `har'st` A

Demonstration: converting a Product of Stops items into Stops of Sum of these items:

> Valid `har'st` A `hjd_'ys` First `ha` Valid `har'st` B = Valid `ha` This `har'st` A > Error `har'st` A `hjd_'ys` First `ha` Valid `har'st` B = Valid `ha` That `har'st` B > Error `har'st` A `hjd_'ys` First `ha` Error `har'st` B = Error `har'st` A > Valid `har'st` A `hjd_'ys` First `ha` Error `har'st` B = Valid `ha` This `har'st` A

Counterpart: label that points to an item that does not exist yet is Fresh.