varkor varkor

Traits as type constructors

This is a demonstration that we may view traits as type constructors: that is, functions from Type to Type. This view is motivated from a categorical perspective of type theory, in which the morphisms of the category take the central role. Cf. subobjects, which are represented by morphisms, rather than objects in a different category.

I'm assuming that the category of types, Type, is bicartesian closed. The set of morphisms between any two objects includes the set of functions denoted by Fn, FnMut and FnOnce in Rust.

	\newcommand{\cat}{\mathscr}
	\newcommand{\psh}{\widehat}
	\newcommand{\smcat}{\mathbb}
	\newcommand{\yo}{よ}

	(* Functions for converting between f32 and Real *)
	f32ToReal[li_]:=SetPrecision[First[ImportString[ExportString[FromDigits[li,2],"UnsignedInteger32"],"Real32"]],Infinity];
	realToF32[x_]:=IntegerDigits[First[ImportString[ExportString[x,"Real32"],"UnsignedInteger32"]],2,32];

	(* Functions for converting between binary strings *)
	binaryF32ToReal[x_]:=f32ToReal@ToExpression@StringSplit[x,""]
	toDegrees[x_] := x/Degree
	realToBinaryF32[x_] := StringJoin[ToString /@ realToF32[x]]

	(* For example: *)

	// ==UserScript==
	// @name WhatsApp Emoticon Preserver
	// @namespace https://gist.github.com/varkor/ca697f6fd59f60b5b9a8aeaa6d7cb341
	// @version 0.5
	// @author varkor
	// @description Disable automatic emoticon → emoji conversion in WhatsApp Web
	// @match https://web.whatsapp.com/
	// @grant none
	// ==/UserScript==