-
Notifications
You must be signed in to change notification settings - Fork 9
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
base: main
Are you sure you want to change the base?
?_ rune #24
Changes from 2 commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
--- | ||
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. | ||
|
||
## Specification | ||
|
||
See https://github.com/urbit/urbit/pull/6656 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Please reproduce the spec here. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. done, and expanded upon it |
||
|
||
## 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. | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. STUN with There was a problem hiding this comment. Choose a reason for hiding this commentThe 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). |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.