?_ rune

UIPS/UIP-0014.md

@@ -0,0 +1,144 @@
+---
+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: Hoon
+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.
+
+`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
+
+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
+
+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
+
+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).