triallax changed the topic of #numbat to: The Official Numbat channel https://numbat.dev | This channel is publicly logged at https://libera.irclog.whitequark.org/numbat | Please read https://workaround.org/getting-help-on-irc/ if you're new to IRC!
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
<sharkdp> !nb fn f(x, y, z) = (x^2 y z^-1 == a^8) && (x^-3 y^-1 z^2 == a^-11) && (x^-2 y z^2 == a^-3)
<Charbot9000> Error: Unknown identifier 'a'.
<sharkdp> !nb unit a
<Charbot9000> unit a: A
<sharkdp> !nb fn f(x, y, z) = (x^2 y z^-1 == a^8) && (x^-3 y^-1 z^2 == a^-11) && (x^-2 y z^2 == a^-3)
<Charbot9000> fn f(x: A², y: A³, z: A⁻¹) -> Bool = (((x² × y × z^(-1)) == (a^8)) && ((x^(-3) × y^(-1) × z²) == (a^(-11)))) && ((x^(-2) × y × z²) == (a^(-3)))
<sharkdp> I invented a fun way to solve systems of linear equations using Numbats type inference algorithm
<sharkdp> The above function encodes the following system of equations:
<sharkdp> # 2x + y - z = 8
<sharkdp> # -3x - y + 2z = -11
<sharkdp> # -2x + y + 2z = -3
<sharkdp> And the solution (x = 2, y = 3, z = -1) can be read off from the inferred types of x, y, and z.
sharkdp has quit [Remote host closed the connection]