Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

?_ rune #24

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
144 changes: 144 additions & 0 deletions UIPS/UIP-0014.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,144 @@
---
uip: 0114
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

please quote the UIP so GH doesn't parse it as octal

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
uip: 0114
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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

STUN with ?_!

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

it's a very cool, entirely unexpected feature!

## 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).