A canonical representation for free left-dioids

RIVAS, EXEQUIEL; POSTAN, EZEQUIEL; JASKELIOFF, MAURO

Bahía Blanca

Congreso; XIV Congreso Dr. Antonio Monteiro; 2017

Dioids (or cubical monoids) were introduced by Marco Grandis in an attempt to decategorify the notion of cubical monad. These algebras can be relaxed in such a way that only left or right absorptions are assumed. Concretely, aleft-dioid is an algebra $D = (D, \oplus, \otimes,  0, 1)$ that satisfies the conditions:- (D1) $(D, \oplus, 0)$ is a monoid- (D2) $(D, \otimes, 1)$ is a monoid- (D3) $0 \otimes x \approx 0$- (D4) $1 \oplus x \approx 1$Motivated by categorical interpretations of functional programs, wefound left-dioids related to computational effects in the presence ofexceptions. In this work we introduce a canonical representation forthe free left-dioid over a set, obtaining an implementation which canbe presented in a language with a simple type system.