[urbit] A few hoon questions

Discussion:

Zach Gotsch

2016-08-15 10:13:41 UTC

Hey I was looking at some of the Hoon resources this weekend and I had a
few questions and things I didn't understand. I hope this is an appropriate
place for my questions.

i)
There seems to be some sort of output formatting for floats, since

(add:rs .0.1 .0.2)

.3e-1

but

(add:rd .~0.1 .~0.2)

.~3.0000000000000004e-1

Where can I see how the pretty-printing in dojo is happening (if that's
even what this is...)?

ii)
I don't think I understand how constant nouns (rocks?) are represented.
%a has aura (mold? not sure of the difference here either) $a, but the raw
value 97
%97 also has raw value 97, but aura $97

I would expect =(%a %97) to be .y, since I don't expect the types to have
any bearing on equality testing. Instead it is an error. I guess my main
question here is "When do types (er, auras?) matter?" Something like (add
%97 1) doesn't cause an error, and produces 98, which I expect if add
doesn't care about types. Side note, casting the rocks seems to prevent the
%.y

iii)
From the docs: "When we print b, or any core, we see that typed noun
printing can't be an invertible function in Hoon". I don't understand why
it's not invertable. Is it because the battery is Nock, and you can't enter
nock code in Hoon?

iv)
@n seems to be a thing but I can't use it at the prompt without causing an
error. Is this like undefined/bottom in haskell?

v)
I was messing around with auras and I was wondering if `@tr`1 was something
like ~s1 (or milliseconds or microseconds). When I typed it into dojo, it
printed all sorts of stuff and overwrote the prompt. What is the stuff that
it prints and why does this happen? (After typing this out, I realized that
it's a runtime error of some kind. Where can I learn how to interpret the
printed stuff?)

vi)
In the documentation, it says ;; applies a mold, asserting fixed point. All
molds should have fixed points for all inputs because they are idempotent,
right? So is this just a function application of the mold and an assertion
that it is, in fact idempotent?

vii)
Is there a way to refer to the last twig in the dojo prompt (like `it` in
ghci)?

viii)
it(@)
~[0 1 2 3 4 5]

I don't understand the type of gulf's output, it isn't a cell, and I
haven't seen `it(@)`. Does `it` mean "iterated". Is `@` a type parameter
here?

I hope this wasn't too much for the mailing list but since the network is
down I haven't been able to bother people on :talk

Zach

--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an email to urbit-dev+***@googlegroups.com.
To post to this group, send email to urbit-***@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Curtis Yarvin

2016-08-15 14:22:57 UTC

Permalink

Not at all, Zach, great questions. I have only one question in
response (Customer Feedback Survey #42): which docs did you read in
which order, and which helped the most?

i) The pretty-printing of floats (and everything) is not in :dojo, but
in hoon.hoon (++co) (specifically in r-co). Note that I didn't write
the floating-point code -- it's a contributor's work (Max Greer).

ii) In older versions of Hoon there was no constraint on equality
testing, because you can test any two nouns for equality. This was
only one of many things in Hoon that horrified people with a
traditional typed FP background. In this case I decided that the
traditionalists were right, because I have seen this check turn up
bugs. On the other hand, most other people who know Hoon are a little
horrified by most of my recent changes, so it could be that I'm just
losing my mojo. In any case, equality testing requires one side of
the test to be a subtype of the other (nest within it).

iii) A core contains compiled Hoon code in Nock form. An invertible
printer would have to decompile it, or something -- basically
impossible. You've lost informatoion.

iv) Ha! This is a bug (if a small one). Do you want to file it?
You'll get valuable Bug Points which may in future be exchangeable for
exciting action figures.

v) This is because (a) we can't statically verify auras (for obvious
reasons, since Hoon is not Coq), and (b) we don't in practice check
them adequately before feeding them to the console, resulting in wacky
formatting for invalid strings (another small bug).

vi) One, Hoon can't actually validate that a mold is idempotent
(because not Coq). Two, ;; doesn't normalize; if (mold a) doesn't
equal a, it crashes. There are cases where normalization is good
practice, but they tend to be the exception, even though defining
molds as normalizers is a good design. For instance, in networking,
Urbit has definitely moved away from Postel's law, which seems to be a
lot less relevant when you have, like, types and stuff.

vii) There isn't but that's a great idea (thanks ghci). There is
history with a kill buffer, though, so ^P^A^K^N^Y will do the same
thing. I'd have to think about how to fit this into the dojo, though,
it's non-obvious.

viii) The "type" output in the prettyprinter is its own thing -- it is
not either a mold or a span, just a thing derived from inspecting the
span. See under "not invertible." In this case, we see that your
structure is a repeating structure of the form {i/item t/tail}, which
happens to be what ++list makes, so we're basically saying it's a
list. If you make this same span with any other mold, though, you'll
get the same results -- all typing in Hoon is structural.

Hey I was looking at some of the Hoon resources this weekend and I had a few
questions and things I didn't understand. I hope this is an appropriate
place for my questions.
i)
There seems to be some sort of output formatting for floats, since

(add:rs .0.1 .0.2)

.3e-1
but

(add:rd .~0.1 .~0.2)

.~3.0000000000000004e-1
Where can I see how the pretty-printing in dojo is happening (if that's even
what this is...)?
ii)
I don't think I understand how constant nouns (rocks?) are represented.
%a has aura (mold? not sure of the difference here either) $a, but the raw
value 97
%97 also has raw value 97, but aura $97
I would expect =(%a %97) to be .y, since I don't expect the types to have
any bearing on equality testing. Instead it is an error. I guess my main
question here is "When do types (er, auras?) matter?" Something like (add
%97 1) doesn't cause an error, and produces 98, which I expect if add
doesn't care about types. Side note, casting the rocks seems to prevent the
%.y
iii)
From the docs: "When we print b, or any core, we see that typed noun
printing can't be an invertible function in Hoon". I don't understand why
it's not invertable. Is it because the battery is Nock, and you can't enter
nock code in Hoon?
iv)
@n seems to be a thing but I can't use it at the prompt without causing an
error. Is this like undefined/bottom in haskell?
v)
like ~s1 (or milliseconds or microseconds). When I typed it into dojo, it
printed all sorts of stuff and overwrote the prompt. What is the stuff that
it prints and why does this happen? (After typing this out, I realized that
it's a runtime error of some kind. Where can I learn how to interpret the
printed stuff?)
vi)
In the documentation, it says ;; applies a mold, asserting fixed point. All
molds should have fixed points for all inputs because they are idempotent,
right? So is this just a function application of the mold and an assertion
that it is, in fact idempotent?
vii)
Is there a way to refer to the last twig in the dojo prompt (like `it` in
ghci)?
viii)
~[0 1 2 3 4 5]
I don't understand the type of gulf's output, it isn't a cell, and I haven't
I hope this wasn't too much for the mailing list but since the network is
down I haven't been able to bother people on :talk
Zach
--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
For more options, visit https://groups.google.com/d/optout.

Anton Dyudin

2016-08-15 15:20:24 UTC

Permalink

Post by Curtis Yarvin
Not at all, Zach, great questions. I have only one question in
response (Customer Feedback Survey #42): which docs did you read in
which order, and which helped the most?
i) The pretty-printing of floats (and everything) is not in :dojo, but
in hoon.hoon (++co) (specifically in r-co). Note that I didn't write
the floating-point code -- it's a contributor's work (Max Greer).
ii) In older versions of Hoon there was no constraint on equality
testing, because you can test any two nouns for equality. This was
only one of many things in Hoon that horrified people with a
traditional typed FP background. In this case I decided that the
traditionalists were right, because I have seen this check turn up
bugs. On the other hand, most other people who know Hoon are a little
horrified by most of my recent changes, so it could be that I'm just
losing my mojo. In any case, equality testing requires one side of
the test to be a subtype of the other (nest within it).
iii) A core contains compiled Hoon code in Nock form. An invertible
printer would have to decompile it, or something -- basically
impossible. You've lost informatoion.
iv) Ha! This is a bug (if a small one). Do you want to file it?
You'll get valuable Bug Points which may in future be exchangeable for
exciting action figures.
v) This is because (a) we can't statically verify auras (for obvious
reasons, since Hoon is not Coq), and (b) we don't in practice check
them adequately before feeding them to the console, resulting in wacky
formatting for invalid strings (another small bug).
vi) One, Hoon can't actually validate that a mold is idempotent
(because not Coq). Two, ;; doesn't normalize; if (mold a) doesn't
equal a, it crashes. There are cases where normalization is good
practice, but they tend to be the exception, even though defining
molds as normalizers is a good design. For instance, in networking,
Urbit has definitely moved away from Postel's law, which seems to be a
lot less relevant when you have, like, types and stuff.
vii) There isn't but that's a great idea (thanks ghci). There is
history with a kill buffer, though, so ^P^A^K^N^Y will do the same
thing. I'd have to think about how to fit this into the dojo, though,
it's non-obvious.
viii) The "type" output in the prettyprinter is its own thing -- it is
not either a mold or a span, just a thing derived from inspecting the
span. See under "not invertible." In this case, we see that your
structure is a repeating structure of the form {i/item t/tail}, which
happens to be what ++list makes, so we're basically saying it's a
list. If you make this same span with any other mold, though, you'll
get the same results -- all typing in Hoon is structural.

Post by Zach Gotsch
Hey I was looking at some of the Hoon resources this weekend and I had a

few

Post by Zach Gotsch
questions and things I didn't understand. I hope this is an appropriate
place for my questions.
i)
There seems to be some sort of output formatting for floats, since

(add:rs .0.1 .0.2)

.3e-1
but

(add:rd .~0.1 .~0.2)

.~3.0000000000000004e-1
Where can I see how the pretty-printing in dojo is happening (if that's

even

Post by Zach Gotsch
what this is...)?
ii)
I don't think I understand how constant nouns (rocks?) are represented.
%a has aura (mold? not sure of the difference here either) $a, but the

raw

Post by Zach Gotsch
value 97
%97 also has raw value 97, but aura $97
I would expect =(%a %97) to be .y, since I don't expect the types to have
any bearing on equality testing. Instead it is an error. I guess my main
question here is "When do types (er, auras?) matter?" Something like (add
%97 1) doesn't cause an error, and produces 98, which I expect if add
doesn't care about types. Side note, casting the rocks seems to prevent

the

Post by Zach Gotsch
%.y
iii)
From the docs: "When we print b, or any core, we see that typed noun
printing can't be an invertible function in Hoon". I don't understand why
it's not invertable. Is it because the battery is Nock, and you can't

enter

Post by Zach Gotsch
nock code in Hoon?
iv)
@n seems to be a thing but I can't use it at the prompt without causing

Post by Zach Gotsch
error. Is this like undefined/bottom in haskell?
v)

something

Post by Zach Gotsch
like ~s1 (or milliseconds or microseconds). When I typed it into dojo, it
printed all sorts of stuff and overwrote the prompt. What is the stuff

that

Post by Zach Gotsch
it prints and why does this happen? (After typing this out, I realized

that

Post by Zach Gotsch
it's a runtime error of some kind. Where can I learn how to interpret the
printed stuff?)
vi)
In the documentation, it says ;; applies a mold, asserting fixed point.

All

Post by Zach Gotsch
molds should have fixed points for all inputs because they are

idempotent,

Post by Zach Gotsch
right? So is this just a function application of the mold and an

assertion

Post by Zach Gotsch
that it is, in fact idempotent?
vii)
Is there a way to refer to the last twig in the dojo prompt (like `it` in
ghci)?
viii)
~[0 1 2 3 4 5]
I don't understand the type of gulf's output, it isn't a cell, and I

haven't

Post by Zach Gotsch
I hope this wasn't too much for the mailing list but since the network is
down I haven't been able to bother people on :talk
Zach
--
You received this message because you are subscribed to the Google Groups
"urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an

<javascript:;>.

Post by Zach Gotsch
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
<javascript:;>.
For more options, visit https://groups.google.com/d/optout.

Raymond Pasco

2016-08-15 16:38:14 UTC

Permalink

iv) One of my "way too fancy to be practical rn" ideas is abbreviation of printed nouns via replacing sections with .^(... %gx /=dojo=/n), which could work on arbitrarily large nouns incl cores and such. Not much you can do if you have to render the whole noun in one go thought, yeah.
Not at all, Zach, great questions. I have only one question in
response (Customer Feedback Survey #42): which docs did you read in
which order, and which helped the most?
i) The pretty-printing of floats (and everything) is not in :dojo, but
in hoon.hoon (++co) (specifically in r-co). Note that I didn't write
the floating-point code -- it's a contributor's work (Max Greer).
ii) In older versions of Hoon there was no constraint on equality
testing, because you can test any two nouns for equality. This was
only one of many things in Hoon that horrified people with a
traditional typed FP background. In this case I decided that the
traditionalists were right, because I have seen this check turn up
bugs. On the other hand, most other people who know Hoon are a little
horrified by most of my recent changes, so it could be that I'm just
losing my mojo. In any case, equality testing requires one side of
the test to be a subtype of the other (nest within it).
iii) A core contains compiled Hoon code in Nock form. An invertible
printer would have to decompile it, or something -- basically
impossible. You've lost informatoion.
iv) Ha! This is a bug (if a small one). Do you want to file it?
You'll get valuable Bug Points which may in future be exchangeable for
exciting action figures.
v) This is because (a) we can't statically verify auras (for obvious
reasons, since Hoon is not Coq), and (b) we don't in practice check
them adequately before feeding them to the console, resulting in wacky
formatting for invalid strings (another small bug).
vi) One, Hoon can't actually validate that a mold is idempotent
(because not Coq). Two, ;; doesn't normalize; if (mold a) doesn't
equal a, it crashes. There are cases where normalization is good
practice, but they tend to be the exception, even though defining
molds as normalizers is a good design. For instance, in networking,
Urbit has definitely moved away from Postel's law, which seems to be a
lot less relevant when you have, like, types and stuff.
vii) There isn't but that's a great idea (thanks ghci). There is
history with a kill buffer, though, so ^P^A^K^N^Y will do the same
thing. I'd have to think about how to fit this into the dojo, though,
it's non-obvious.
viii) The "type" output in the prettyprinter is its own thing -- it is
not either a mold or a span, just a thing derived from inspecting the
span. See under "not invertible." In this case, we see that your
structure is a repeating structure of the form {i/item t/tail}, which
happens to be what ++list makes, so we're basically saying it's a
list. If you make this same span with any other mold, though, you'll
get the same results -- all typing in Hoon is structural.

Hey I was looking at some of the Hoon resources this weekend and I had a few
questions and things I didn't understand. I hope this is an appropriate
place for my questions.
i)
There seems to be some sort of output formatting for floats, since

(add:rs .0.1 .0.2)

.3e-1
but

(add:rd .~0.1 .~0.2)

.~3.0000000000000004e-1
Where can I see how the pretty-printing in dojo is happening (if that's even
what this is...)?
ii)
I don't think I understand how constant nouns (rocks?) are represented.
%a has aura (mold? not sure of the difference here either) $a, but the raw
value 97
%97 also has raw value 97, but aura $97
I would expect =(%a %97) to be .y, since I don't expect the types to have
any bearing on equality testing. Instead it is an error. I guess my main
question here is "When do types (er, auras?) matter?" Something like (add
%97 1) doesn't cause an error, and produces 98, which I expect if add
doesn't care about types. Side note, casting the rocks seems to prevent the
%.y
iii)
From the docs: "When we print b, or any core, we see that typed noun
printing can't be an invertible function in Hoon". I don't understand why
it's not invertable. Is it because the battery is Nock, and you can't enter
nock code in Hoon?
iv)
@n seems to be a thing but I can't use it at the prompt without causing an
error. Is this like undefined/bottom in haskell?
v)
like ~s1 (or milliseconds or microseconds). When I typed it into dojo, it
printed all sorts of stuff and overwrote the prompt. What is the stuff that
it prints and why does this happen? (After typing this out, I realized that
it's a runtime error of some kind. Where can I learn how to interpret the
printed stuff?)
vi)
In the documentation, it says ;; applies a mold, asserting fixed point. All
molds should have fixed points for all inputs because they are idempotent,
right? So is this just a function application of the mold and an assertion
that it is, in fact idempotent?
vii)
Is there a way to refer to the last twig in the dojo prompt (like `it` in
ghci)?
viii)
~[0 1 2 3 4 5]
I don't understand the type of gulf's output, it isn't a cell, and I haven't
I hope this wasn't too much for the mailing list but since the network is
down I haven't been able to bother people on :talk
Zach
--
You received this message because you are subscribed to the Google Groups
"urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "urbit" group.
For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups "urbit" group.
For more options, visit https://groups.google.com/d/optout.

Curtis Yarvin

2016-08-15 16:58:07 UTC

Permalink

No, it's just a gnarly little bug. To be useful, it would have to be
consistent.

Hey I was looking at some of the Hoon resources this weekend and I had a few
questions and things I didn't understand. I hope this is an appropriate
place for my questions.
i)
There seems to be some sort of output formatting for floats, since

(add:rs .0.1 .0.2)

.3e-1
but

(add:rd .~0.1 .~0.2)

.~3.0000000000000004e-1
Where can I see how the pretty-printing in dojo is happening (if that's even
what this is...)?
ii)
I don't think I understand how constant nouns (rocks?) are represented.
%a has aura (mold? not sure of the difference here either) $a, but the raw
value 97
%97 also has raw value 97, but aura $97
I would expect =(%a %97) to be .y, since I don't expect the types to have
any bearing on equality testing. Instead it is an error. I guess my main
question here is "When do types (er, auras?) matter?" Something like (add
%97 1) doesn't cause an error, and produces 98, which I expect if add
doesn't care about types. Side note, casting the rocks seems to prevent the
%.y
iii)
From the docs: "When we print b, or any core, we see that typed noun
printing can't be an invertible function in Hoon". I don't understand why
it's not invertable. Is it because the battery is Nock, and you can't enter
nock code in Hoon?
iv)
@n seems to be a thing but I can't use it at the prompt without causing an
error. Is this like undefined/bottom in haskell?
v)
like ~s1 (or milliseconds or microseconds). When I typed it into dojo, it
printed all sorts of stuff and overwrote the prompt. What is the stuff that
it prints and why does this happen? (After typing this out, I realized that
it's a runtime error of some kind. Where can I learn how to interpret the
printed stuff?)
vi)
In the documentation, it says ;; applies a mold, asserting fixed point. All
molds should have fixed points for all inputs because they are idempotent,
right? So is this just a function application of the mold and an assertion
that it is, in fact idempotent?
vii)
Is there a way to refer to the last twig in the dojo prompt (like `it` in
ghci)?
viii)
~[0 1 2 3 4 5]
I don't understand the type of gulf's output, it isn't a cell, and I haven't
I hope this wasn't too much for the mailing list but since the network is
down I haven't been able to bother people on :talk
Zach
--
You received this message because you are subscribed to the Google Groups
"urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
For more options, visit https://groups.google.com/d/optout.

Zach Gotsch

2016-08-15 18:01:23 UTC

Permalink

I started out with the Urbytes, which were great and super easy to follow.
After I read the three which are available I dived into the Hoon guide (in
order, freely disengaging if I didn't feel ready for stuff or didn't see
the point of things yet). It was much denser and more difficult. I think I
would have benefitted from some more depth in the examples at
http://urbit.org/docs/hoon/examples/.

i) Cool, I'll check it out.

ii) Heh, I am just one of those traditionalist type-lovers, but I kind of
expected `=` to be the sort of function which doesn't hold truck with
types. In Urbyte 0, it mentions that types are just unsigned integers of
arbitrary length. `=` shows that this isn't quite the whole story. In my
opinion (which probably isn't worth much yet, admittedly!) `=` checking
types will keep a lot of silly bugs from happening, and the pragmatic thing
to do is to keep an eye out for them.

iii) Got it.

iv) Filed, https://github.com/urbit/urbit/issues/769

v) Yes, meant `@dr` thanks Anton. Brain wires got crossed, everything makes
sense again!

vi) Ah yes, I see now after reading your answer and the documentation a
little more closely.

vii) Is possible to do something like `=.(it <previous twig value> .)` and
make that the new subject? Disclaimer: this didn't work in my dojo and I'm
not sure why, so I'm guessing the answer is "no, and I'm not sure why you
would think that".

viii) Ah, didn't realize that the type was its own thing. Makes more sense
now.

Thanks for the great answers.

Post by Curtis Yarvin
No, it's just a gnarly little bug. To be useful, it would have to be
consistent.

Post by Anton Dyudin
iv) One of my "way too fancy to be practical rn" ideas is abbreviation

of printed nouns via replacing sections with .^(... %gx /=dojo=/n), which
could work on arbitrarily large nouns incl cores and such. Not much you can
do if you have to render the whole noun in one go thought, yeah.
text though, was the core error %bad-utf8?

Post by Anton Dyudin
Not at all, Zach, great questions. I have only one question in
response (Customer Feedback Survey #42): which docs did you read in
which order, and which helped the most?
i) The pretty-printing of floats (and everything) is not in :dojo, but
in hoon.hoon (++co) (specifically in r-co). Note that I didn't write
the floating-point code -- it's a contributor's work (Max Greer).
ii) In older versions of Hoon there was no constraint on equality
testing, because you can test any two nouns for equality. This was
only one of many things in Hoon that horrified people with a
traditional typed FP background. In this case I decided that the
traditionalists were right, because I have seen this check turn up
bugs. On the other hand, most other people who know Hoon are a little
horrified by most of my recent changes, so it could be that I'm just
losing my mojo. In any case, equality testing requires one side of
the test to be a subtype of the other (nest within it).
iii) A core contains compiled Hoon code in Nock form. An invertible
printer would have to decompile it, or something -- basically
impossible. You've lost informatoion.
iv) Ha! This is a bug (if a small one). Do you want to file it?
You'll get valuable Bug Points which may in future be exchangeable for
exciting action figures.
v) This is because (a) we can't statically verify auras (for obvious
reasons, since Hoon is not Coq), and (b) we don't in practice check
them adequately before feeding them to the console, resulting in wacky
formatting for invalid strings (another small bug).
vi) One, Hoon can't actually validate that a mold is idempotent
(because not Coq). Two, ;; doesn't normalize; if (mold a) doesn't
equal a, it crashes. There are cases where normalization is good
practice, but they tend to be the exception, even though defining
molds as normalizers is a good design. For instance, in networking,
Urbit has definitely moved away from Postel's law, which seems to be a
lot less relevant when you have, like, types and stuff.
vii) There isn't but that's a great idea (thanks ghci). There is
history with a kill buffer, though, so ^P^A^K^N^Y will do the same
thing. I'd have to think about how to fit this into the dojo, though,
it's non-obvious.
viii) The "type" output in the prettyprinter is its own thing -- it is
not either a mold or a span, just a thing derived from inspecting the
span. See under "not invertible." In this case, we see that your
structure is a repeating structure of the form {i/item t/tail}, which
happens to be what ++list makes, so we're basically saying it's a
list. If you make this same span with any other mold, though, you'll
get the same results -- all typing in Hoon is structural.

Post by Zach Gotsch
Hey I was looking at some of the Hoon resources this weekend and I

had a few