?- E = "pop dup dup * swap abs rollup dup * swap - +", joy(E, Si, So). E = "pop dup dup * swap abs ro...p - +", Si = [_56410, int(_56422), int(_56432)|_

?- E = "pop dup dup * swap abs rollup dup * swap - +", joy(E, Si, So). E = "pop dup dup * swap abs ro...p - +", Si = [_56410, int(_56422), int(_56432)|_56428], So = [int(_56454)|_56428], _56422 in 0..sup, _56500+_56422#=_56496, _56422+1#=_56520, _56422^2#=_56544, _56500+_56544#=_56454, _56544 in 0..sup, _56496 in 0..sup, _56432^2#=_56496, _56520 in 1..sup ; E = "pop dup dup * swap abs ro...p - +", Si = [_57392, int(_57404), int(_57414)|_57410], So = [int(_57436)|_57410], _57404 in inf.. -1, _57482+_57404#=0, _57404+1#=_57502, _57404^2#=_57526, _57482 in 1..sup, _57578+_57482#=_57574, _57578+_57526#=_57436, _57526 in 1..sup, _57574 in 0..sup, _57414^2#=_57574, _57502 in inf..0 ; false. It's a Prolog query with two solutions (because the input to abs could be positive or negative) showing the input and output stack effects (the type signature) and the CLP(FD) constraints between the input and output integers. It's a little hard to read, I know, but the code that performs the type inference and constraint generation/recording is very brief and elegant. ( It's a work-in-progress: https://git.sr.ht/~sforman/Thun/tree/master/source/thun.pl https://git.sr.ht/~sforman/Thun/tree/master/source/thun.pl ) - - - - FWIW I messed about with a Python implementation of Joy (another concatinative language) and I have some notebooks that might be interesting: https://joypy.osdn.io/notebooks/index.html https://joypy.osdn.io/notebooks/index.html