Stream: general

Topic: match on !


RalfJ (Nov 23 2018 at 07:08, on Zulip):

@Mazdak Farrokhzad hi there :D

centril (Nov 23 2018 at 07:08, on Zulip):

this UI makes no sense :confused: why did I end up in staged-compilation...? :confused:

RalfJ (Nov 23 2018 at 07:08, on Zulip):

"so match b { x => ... } where b: &! does not dereference, and hence no UB".... it seems to me that then it means that let b: &! = ...; match b {} won't typeck

maybe

RalfJ (Nov 23 2018 at 07:08, on Zulip):

this UI makes no sense :/ why did I end up in staged-compilation...? :/

it's got a slightly steeper learning curve than Discord, true

RalfJ (Nov 23 2018 at 07:09, on Zulip):

but then, so does Rust, so I am sure you can manage :P

centril (Nov 23 2018 at 07:09, on Zulip):

nah; Rust didn't really have a steep learning curve for me ;)

RalfJ (Nov 23 2018 at 07:09, on Zulip):

so for matches, I think we should have a pattern ! for "this is a 0-variant enum"

RalfJ (Nov 23 2018 at 07:10, on Zulip):

and if a pattern contains a ! it needs no code

RalfJ (Nov 23 2018 at 07:10, on Zulip):

so, with b: !, could could do match b { ! }

centril (Nov 23 2018 at 07:10, on Zulip):

Agda does something similar iirc

RalfJ (Nov 23 2018 at 07:10, on Zulip):

with b: (!, i32) you could do match b { (!, _) }

RalfJ (Nov 23 2018 at 07:10, on Zulip):

and with b: &!, you could do match b { &! }

RalfJ (Nov 23 2018 at 07:11, on Zulip):

with b: Result<T, !>, you could do match b { Err(!), Ok(t) => ... }

RalfJ (Nov 23 2018 at 07:11, on Zulip):

and any of these would be UB do actually ever "hit" the ! branch

RalfJ (Nov 23 2018 at 07:11, on Zulip):

as that would be "reading the disrciminant of an empty enum/!"

centril (Nov 23 2018 at 07:11, on Zulip):

https://agda.readthedocs.io/en/v2.5.2/language/function-definitions.html#absurd-patterns

RalfJ (Nov 23 2018 at 07:11, on Zulip):

so this gives us a language to talk about pattern matching with empty types in a precise way

RalfJ (Nov 23 2018 at 07:12, on Zulip):

and then we can talk about syntactic sugar and automatically introducing such patterns

centril (Nov 23 2018 at 07:12, on Zulip):

I do like the idea of a ! pattern; it provides an in-language desugaring

RalfJ (Nov 23 2018 at 07:12, on Zulip):

like, match b {} with b: ! could desugar to match b { ! }

centril (Nov 23 2018 at 07:12, on Zulip):

which is good for teaching

RalfJ (Nov 23 2018 at 07:12, on Zulip):

and we have a way to tweak how smart we make this sugar

RalfJ (Nov 23 2018 at 07:12, on Zulip):

niko wrote this down somewhere but I am not sure where... IRLO I think?

centril (Nov 23 2018 at 07:13, on Zulip):

yeah; this was the thing that Niko talked about in his blog post; http://smallcultfollowing.com/babysteps/blog/2018/08/13/never-patterns-exhaustive-matching-and-uninhabited-types-oh-my/

centril (Nov 23 2018 at 07:13, on Zulip):

https://internals.rust-lang.org/t/blog-post-never-patterns-exhaustive-matching-and-uninhabited-types/8197

RalfJ (Nov 23 2018 at 07:14, on Zulip):

ah yes, that was it

RalfJ (Nov 23 2018 at 07:14, on Zulip):

he wrote that post after we had a long chat

centril (Nov 23 2018 at 07:14, on Zulip):

I'm down with the general idea of match b { ! }

RalfJ (Nov 23 2018 at 07:15, on Zulip):

and yes I am not surprised agda has something like this

RalfJ (Nov 23 2018 at 07:16, on Zulip):

they have fancy pattern matching and a decent type system

RalfJ (Nov 23 2018 at 07:16, on Zulip):

such patterns are pretty much a given then, I think

centril (Nov 23 2018 at 07:16, on Zulip):

yup

centril (Nov 23 2018 at 07:16, on Zulip):

(pressing r all the time is annoying...)

RalfJ (Nov 23 2018 at 07:17, on Zulip):

so why do you?

centril (Nov 23 2018 at 07:17, on Zulip):

oh you can press enter as well

RalfJ (Nov 23 2018 at 07:18, on Zulip):

once you are in a topic, you can just chat like with any other service

RalfJ (Nov 23 2018 at 07:18, on Zulip):

except that you also get keyboard-only navigation for quoting and mentioning people :D

centril (Nov 23 2018 at 07:19, on Zulip):

@RalfJ yeah but in Discord I don't have to press enter/r and I can just click the message box and stay there

RalfJ (Nov 23 2018 at 07:19, on Zulip):

yeah I do that here too

RalfJ (Nov 23 2018 at 07:19, on Zulip):

type message, enter-to-send. type message, enter-to-send.

centril (Nov 23 2018 at 07:19, on Zulip):

but how? you first have to press enter/r or click "reply"?

RalfJ (Nov 23 2018 at 07:20, on Zulip):

no? you are already in the topic

RalfJ (Nov 23 2018 at 07:20, on Zulip):

it shows the topic above the msg box, to the right of the stream

centril (Nov 23 2018 at 07:20, on Zulip):

yes but to send a message?

RalfJ (Nov 23 2018 at 07:20, on Zulip):

...?

RalfJ (Nov 23 2018 at 07:21, on Zulip):

after sending a message, the text box at the bottom stays open

RalfJ (Nov 23 2018 at 07:21, on Zulip):

you just type the next message

RalfJ (Nov 23 2018 at 07:21, on Zulip):

I am confused, never had any problem^^

centril (Nov 23 2018 at 07:21, on Zulip):

it doesn't for me :confused:

RalfJ (Nov 23 2018 at 07:21, on Zulip):

I think per default it might use Ctrl-Enter for sending, there is a checkbox to configure that below the chat box

centril (Nov 23 2018 at 07:21, on Zulip):

it gets closed and stuff

centril (Nov 23 2018 at 07:21, on Zulip):

yeah I checked that box

RalfJ (Nov 23 2018 at 07:21, on Zulip):

it only gets closed when I click on a new message

centril (Nov 23 2018 at 07:22, on Zulip):

test

RalfJ (Nov 23 2018 at 07:22, on Zulip):

or use the arrow keys to navigate

centril (Nov 23 2018 at 07:22, on Zulip):

oh... this is some shitty UX

centril (Nov 23 2018 at 07:22, on Zulip):

anyways... back to patterns...

RalfJ (Nov 23 2018 at 07:23, on Zulip):

not sure what you did to close the box?^^

RalfJ (Nov 23 2018 at 07:23, on Zulip):

I had way more trouble with discord's UX than this one, FWIW (subscribing me to all channels of the server at once, seriously? separating PMs from channels? the mouse taking precedence over the keyboard during @autocomplection? not to mention an unreadable default font+size...)

RalfJ (Nov 23 2018 at 07:24, on Zulip):

but I guess the perfect chat service has still to be created

RalfJ (Nov 23 2018 at 07:24, on Zulip):

ah, there's nothing like a train getting delayed when you have to catch a flight

centril (Nov 23 2018 at 07:25, on Zulip):

where are you going?

RalfJ (Nov 23 2018 at 07:25, on Zulip):

RustFest :D

centril (Nov 23 2018 at 07:25, on Zulip):

cool

Last update: Nov 22 2019 at 00:10UTC