hoon: add rune ?_, equality test w type refinement

[xiphiness]

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 equality. Most notably, this introduces new types of polymorphism with wet gates, particularly, I have managed to make work a dependently typed map, which could perhaps even be used for dependently typed axals later on.

I haven't included any changes to e.g. +by to fully exploit this yet, though I have tested this out on my own by replacing put and get by:

++  put                                               ::  adds key-value pair
  ~/  %put
  |*  [b=* c=*]
  |-  ^+  a
  ?~  a
    [[b c] ~ ~]
  ?:  ?_(b p.n.a)
    ?:  =(c q.n.a)
      a
    a(n [b c])
  ?:  (gor b p.n.a)
    =+  d=$(a l.a)
    ?>  ?=(^ d)
    ?:  (mor p.n.a p.n.d)
      a(l d)
    d(r a(l r.d))
  =+  d=$(a r.a)
  ?>  ?=(^ d)
  ?:  (mor p.n.a p.n.d)
    a(r d)
  d(l a(r l.d))
::
++  get                                               ::  grab value by key
  ~/  %get
  |*  b=*
  |-  ^-  (unit _?>(&(?=(^ a) ?_(b p.n.a)) q.n.a))
  ?~  a
    ~
  ?:  ?_(b p.n.a)
    (some q.n.a)
  ?:  (gor b p.n.a)
    $(a l.a)
  $(a r.a)

edit: for some reason i stupidly named the branch x/wtbr, and not x/wtcb. oh well!

[xiphiness]

actually, suddenly occurs to me this can be added to .= by only modifying +chip, i think. just check if its a %dtts, then check if the latter hoon is a %wing, if not, do nothing, or if so, +cool

(I think, it might be that the magic that happens in the +ah core is necessary for it to work in chip with ?:)

[xiphiness]

oookay we have some mull-bonks in the map case, i guess, because i was testing it with play rather than mint...

(in various configurations, have reached mull-bonk-a and mull-bonk-c, c being the main case im dealing w rn)

[ohAitch]

I would expect adding it to .= to break a lot that is relying on it being a pure value comparison, and in particular for the codebase to contain some ?: =(%foo x) that are not ?: ?=(%foo x) to specifically avoid type side-effects.

[xiphiness]

oh, yeah definitely, and note the various times we use =(~ list) instead of ?~ precisely so we don't refine the type

i think what's happening with the mull-bonk-c is that the lose case is losing too much. basically, we should only lose if ?_(a b) a is a constant or completely made of constants

edit:
changing line 9700 from

    ?:  ?=([%wthx *] gen)

to

    ?:  &(how ?=([%wthx *] gen))

did not fix the problem

[ohAitch]

Yep, apologies if I'm stating the obvious!

[xiphiness]

i think i've figured out the issue.

in the %wtcl case of mull, when it loses in the dox case, the type of e.g. b in (~(get by a) b) is * in the dox case, so when we ?_(b p.n.a) the latter case of the ?: is void. hackish, but i think it might be fine to add another flag to chip that says if its wet, in which case, do not apply ?_ restriction, and use that in the dox case

i still feel like not applying ?_ in the lose case should fix this, but seems not to be

[xiphiness]

oops, i did not add the how test in chip to my new rune but to wthx. this fixed the issue!

line 9698

    ?:  ?=([%wtcb *] gen)

to

    ?:  &(how ?=([%wtcb *] gen))

pleased to report that dependently typed axals do work! however, it seems like type checking is nearly exponential on the size of the path, like absurdly slow, takes like 3 seconds for a path of length 4, gasing a list of 7 paths of length 0 to 4 has been taking minutes and still isn't done. i wonder why that is. also, there's a few things i would /like/ to get working, but is probably far less an issue with this PR and more to do with wet gates more broadly, such as, axals where the file is definitely or definitely not nil, axals where the dir is definitely nil, or definitely of a particular hardcoded structure where the keys are a finite list of constants and so one knows where in the map they lie, and then perhaps more speculatively, it might already work, i'm not sure, replacing faces with aliases, e.g. the u in the fil, or the n, p, and q in the dir, so that the more specific type when mull'd still has those wings resolve, but can by-pass them when consuming it.

[jalehman]

@xiphiness Not sure the status of this, but if you want to keep moving it forward, this is going to need a UIP