Was looking forward to this. I was trying to figure out the Scott encoding for data since the original untyped calculus post, so it's nice to see it treated here.
I think there is a viable Scott encoding in the UCC with a single stack by utilising order of values on the stack. C'_i would then be a series of i - 1 `drop`s followed by N - i `nip`s and an `apply` (where `nip` is `swap drop`).
`quote_n` was already defined in the previous post (the one on UCC) which is enough to define Scott encoding on a single stack using an analogous method as the UMCC post.
I came to this post looking for a typing system for a concatenative language and I'm really looking forward to Scott explaining it.
`quote_n` was already defined in the previous post (the one on UCC) which is enough to define Scott encoding on a single stack using an analogous method as the UMCC post.
I came to this post looking for a typing system for a concatenative language and I'm really looking forward to Scott explaining it.