Module

Data.Pointed.Distributivity

Package
purescript-pointed
Repository
vladciobanu/purescript-pointed

This module defines distributivity laws between Can, Smash, and Wedge.

The examples assume that the pointed modules are imported qualified:

import Data.Pointed.Can as C
import Data.Pointed.Smash as S
import Data.Pointed.Wedge as W

#smashWedge Source

smashWedge :: forall c b a. Smash (Wedge a b) c -> Wedge (Smash a c) (Smash b c)

smashWedge returns W.Non in all cases except:

  • S.Two (W.One a) c, in which case it returns W.One (S.Two a c)
  • S.Two (W.Eno b) c, in which case it returns W.Eno (S.Two b c)

#wedgeSmash Source

wedgeSmash :: forall c b a. Wedge (Smash a c) (Smash b c) -> Smash (Wedge a b) c

wedgeSmash returns S.Non in all cases except:

  • W.One (S.Two a c), in which case it returns S.Two (W.One a) c
  • W.Eno (S.Two b c), in which case it returns S.Two (W.Eno b) c

#smashCan Source

smashCan :: forall c b a. Smash (Can a b) c -> Can (Smash a c) (Smash b c)

smashCan returns C.Non unless its input is S.Two can c, in which case, depending on can:

  • C.Non goes to C.Non
  • C.One a goes to C.One (S.Two a c)
  • C.Eno b goes to C.Eno (S.Two b c)
  • C.Two a b goes to C.Two (S.Two a c) (S.Two b c)

#canSmash Source

canSmash :: forall c b a. Can (Smash a c) (Smash b c) -> Smash (Can a b) c

canSmash returns S.Non except when:

C.One (S.Two a c) goes to S.Two (C.One a) c C.Eno (S.Two b c) goes to S.Two (C.Eno b) c C.Two (S.Two a c) goes to S.Two (C.Two a b) c