From 0082c693947771b09dc1c8bfaa02f6cf017d3bae Mon Sep 17 00:00:00 2001 From: xiphiness Date: Mon, 21 Aug 2023 13:40:59 -0600 Subject: [PATCH 1/3] ?_ rune See markdown file. Also, https://github.com/urbit/urbit/pull/6656#issuecomment-1586547520 should adopt this. --- UIPS/UIP-0014.md | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 UIPS/UIP-0014.md diff --git a/UIPS/UIP-0014.md b/UIPS/UIP-0014.md new file mode 100644 index 0000000..ec7cd16 --- /dev/null +++ b/UIPS/UIP-0014.md @@ -0,0 +1,32 @@ +--- +uip: 0114 +title: ?_ rune, noun equality restricts type to left parameter +description: for use with dependently typed maps and other related value-based type inference +author: ~sarpen-laplux (@xiphiness) +status: Draft +type: Standards Track +category: Kernel +created: ~2023.8.9 +--- + +## Abstract + +This PR introduces a new rune ?_(a=hoon b=wing), subject to renaming, whose compiled nock is equivalent to .=, but refines the type of b to that of a on noun equality. + +## Specification + +See https://github.com/urbit/urbit/pull/6656 + +## Rationale + +This procedure can be generalized to work with arbitrary ships, but it's not necessary that it be used for anyone other than our galaxy until we either start forwarding through stars, or need some keep-alive mechanism for "sticky" scry requests. Both of those are planned for the future. The current design keeps formal pings from /app/ping to the rest of the (non-galaxy) sponsorship hierarchy. These could be removed, since galaxies can statelessly forward packets from the sponsor star to the sponsee. + +Initially only galaxies will need to act as STUN servers, but any ship could support STUN requests. These could be used to check connectivity with other ships outside of the event loop, and, if additionally listening on a standard port, could provide useful service to applications running outside of urbit (such as webrtc clients). + +## Backwards Compatibility + +This PR properly would at least modify map and ordered map, and should make sure that this doesn't break compilation everywhere those are used. + +## Copyright + +Copyright and related rights waived via [CC0](../LICENSE.md). From ab60c8ce7f1960d81964bfafa9306541b613a40b Mon Sep 17 00:00:00 2001 From: xiphiness Date: Mon, 21 Aug 2023 14:20:13 -0600 Subject: [PATCH 2/3] ?_ does *not* implement STUN --- UIPS/UIP-0014.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/UIPS/UIP-0014.md b/UIPS/UIP-0014.md index ec7cd16..fc08f35 100644 --- a/UIPS/UIP-0014.md +++ b/UIPS/UIP-0014.md @@ -5,8 +5,8 @@ description: for use with dependently typed maps and other related value-based t author: ~sarpen-laplux (@xiphiness) status: Draft type: Standards Track -category: Kernel -created: ~2023.8.9 +category: Hoon +created: ~2023.8.21 --- ## Abstract @@ -19,9 +19,7 @@ See https://github.com/urbit/urbit/pull/6656 ## Rationale -This procedure can be generalized to work with arbitrary ships, but it's not necessary that it be used for anyone other than our galaxy until we either start forwarding through stars, or need some keep-alive mechanism for "sticky" scry requests. Both of those are planned for the future. The current design keeps formal pings from /app/ping to the rest of the (non-galaxy) sponsorship hierarchy. These could be removed, since galaxies can statelessly forward packets from the sponsor star to the sponsee. - -Initially only galaxies will need to act as STUN servers, but any ship could support STUN requests. These could be used to check connectivity with other ships outside of the event loop, and, if additionally listening on a standard port, could provide useful service to applications running outside of urbit (such as webrtc clients). +Dependently typed maps. Dependently typed axals too, but as mentioned in PR, it seems exponential or factorial on the number of paths with gas, or something. ## Backwards Compatibility From 52cfb66e0a90922288227f1ee15b47d6ba0d2d66 Mon Sep 17 00:00:00 2001 From: xiphiness Date: Mon, 2 Oct 2023 05:31:22 -0600 Subject: [PATCH 3/3] Update UIP-0014.md --- UIPS/UIP-0014.md | 118 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 116 insertions(+), 2 deletions(-) diff --git a/UIPS/UIP-0014.md b/UIPS/UIP-0014.md index fc08f35..16946ae 100644 --- a/UIPS/UIP-0014.md +++ b/UIPS/UIP-0014.md @@ -11,11 +11,125 @@ created: ~2023.8.21 ## Abstract -This PR introduces a new rune ?_(a=hoon b=wing), subject to renaming, whose compiled nock is equivalent to .=, but refines the type of b to that of a on noun equality. +This PR introduces a new rune ?_(a=hoon b=wing), subject to renaming, whose compiled nock is equivalent to `.=`, but refines the type of `b` to that of `a` on noun equality. + +`a` is just any hoon, rather than a mold as in ?= + +The `gain` case is satisfied whenever equality is achieved. In fact, this could be used as an alternative to mold normalization to a constant, e.g. + +```hoon +> =+ a=`*`[%foo ~nec] ?> ?_([%foo p=~nec] a) a +[%foo p=~nec] +```` + +But the chief inspiration is for a map whose values are dependent on the value of the key, here's a working example using an altered form of +by to use these runes: +https://gist.github.com/xiphiness/f45f3d64d9aaa53831b8f9ab1c69e450 + +For the `lose` case, a new gate +const:ut is added, which recurses through the type, returning `&` if it boils down to cells and constant atoms, and `|` otherwise. +If the type of the first argument could have multiple different values, than a negative equality test does not allow us to refine the type. ## Specification -See https://github.com/urbit/urbit/pull/6656 +The rune added is defined + +```hoon + [%wtcb p=hoon q=wing] :: ?_ if q equals p +``` + +then we have wtcb:ah + +```hoon + ++ wtcb |=(sic=hoon (gray [%wtcb (blue sic) puce])) +``` +for use in the parser expander + +```hoon + ++ txcb |. %+ cook |= [a=hoon b=tiki] + (~(wtcb ah b) a) + ;~(gunk loaf teak) +``` + +The macro expansion in `+open:ap` is + +```hoon + [%wtcb *] [%dtts p.gen [%wing q.gen]] +``` + +For the +lose case, we introduce a gate `+const:ut` is + +```hoon + ++ const + ^- ? + =< !=(~ .) + =| seg=(set type) + |- ^- (unit *) + ?- sut + %void ~ + %noun ~ + [%atom *] q.sut + [%cell *] (both $(sut p.sut) $(sut q.sut)) + [%core *] ~ + [%face *] $(sut q.sut) + [%fork *] ?~ fok=~(tap in p.sut) ~ + ?~ i=%_($ sut i.fok) ~ + ?.((lien t.fok |=(type =(i ^$(sut +<)))) ~ i) + [%hint *] $(sut q.sut) + [%hold *] ?: (~(has in seg) sut) ~ + %= $ + sut repo + fan (~(put in fan) +.sut) + == == +``` + +And finally, in +chip:ut, we introduce our case: +``` + ?: ?=([%wtcb *] gen) + =/ p (play p.gen) + ?. |(how const(sut p)) sut + (cool how q.gen p) +``` + +Here is an example of the aforementioned map example +```hoon +> => dap + => |% + +$ my-pair $%([p=[%a p=@ux] q=[%aa p=@p]] [p=[%b p=@p] q=[%bb p=@ud]] [p=[%c p=@ud] q=[%cc p=@ux]]) + -- + =/ a (~(gas by *(tree my-pair)) `(list my-pair)`~[[a+0x123 aa+~zod] [b+~nec bb+120] [c+123 cc+0xdead.beef]]) + =/ b [(~(get by a) a+0x123) (~(get by a) b+~nec) (~(get by a) c+123)] + [-:!>(b) b] +[#t/[u([%aa p=@p]) u([%bb p=@ud]) u([%cc p=@ux])] [~ [%aa p=~zod]] [~ [%bb p=120]] [~ [%cc p=0xdead.beef]]] +``` + +This can also be used as an alternative to ?= or mold normalization in the case one is dealing with constants. + +Here's a few examples showing both this and other use cases: +```hoon +> =+ a=`$%([%foo p=@p] [%bar p=@ux])`[%foo ~zod] ?: ?_([%foo ~zod] a) -:!>(a) -:!>(a) +#t/[%foo p=@p] +> =+ a=`$%([%foo p=@p] [%bar p=@ux])`[%bar 0x123] ?: ?_([%bar 0x123] a) -:!>(a) -:!>(a) +#t/[%bar p=@ux] +> =+ a=`*`[%foo ~nec] ?: ?_([%foo p=~nec] a) -:!>(a) -:!>(a) +#t/[%foo p=@p] +> =+ a=`*`[%foo ~nec] ?: ?_([%foo p=%~nec] a) -:!>(a) -:!>(a) +#t/[%foo p=%~nec] +> =+ a=`*`[%foo ~nec] ?: ?_([%foo p=%~zod] a) -:!>(a) -:!>(a) +#t/?(@ [* *]) +> =+ a=`$%([%foo p=@p] [%bar p=@ux])`[%foo ~nec] ?: ?=(%foo -.a) -:!>(a) -:!>(a) +#t/[%foo p=@p] +> =+ a=`$%([%foo p=@p] [%bar p=@ux])`[%bar 0x123] ?: ?=(%foo -.a) -:!>(a) -:!>(a) +#t/[%bar p=@ux] +> =+ a=`$%([%foo p=_%~nec] [%bar p=@ux])`[%foo %~nec] ?: ?=([%foo %~nec] a) -:!>(a) -:!>(a) +#t/[%foo p=%~nec] +> =+ a=`$%([%foo p=_%~nec] [%bar p=@ux])`[%bar 0x123] ?: ?=([%foo %~nec] a) -:!>(a) -:!>(a) +#t/[%bar p=@ux] +> =+ a=`$%([%foo p=@p] [%bar p=@ux])`[%bar 0x123] ?: ?=([%foo %~nec] a) -:!>(a) -:!>(a) +#t/?([%bar p=@ux] [%foo p=@p]) +> =+ a=`$%([%foo p=_%~nec] [%bar p=@ux])`[%foo %~nec] ?: ?=([%foo %~nec] a) -:!>(a) -:!>(a) +#t/[%foo p=%~nec] +> =+ a=`$%([%foo p=_%~nec] [%bar p=@ux])`[%bar 0x123] ?: ?=([%foo %~nec] a) -:!>(a) -:!>(a) +#t/[%bar p=@ux] +``` ## Rationale