Conor Mc Bride @pigworker@types.pl
re: bidirectional typing
Funny, though. It took me a while to figure out that sauce for the meta-goose is sauce for the object-gander. When you define an "indexed inductive family", it's good to think about whether each index is coming or going.
Exercise: define (by hook, crook, or induction-recursion) the well scoped, well typed, unhyphenated terms of the simply typed lambda calculus, in such a way that the argument type in an application is stored nowhere, not even at 0 quantity.
bidirectional typing
https://pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism/
which begins
I like my type systems to be bidirectional. Different people mean different things by the word “bidirectional”, and I’m one of them. Some people relate the notion to “polarity”, and I’m not one of them.
I just used "Milner" as a verb and it felt filthy but wonderful.
The only acceptable proof is "by inspection".
Pay attention to how you talk about the context in typing rules. Don't talk about what's none of your business. In intuitionistic systems, you should never talk about the shared context left of the turnstile: you should talk only of its local extensions in rule premises. Even that much imposes good discipline that makes you make rule systems which work. And there's much more where that came from.
I'm not actually dead. I'm hiding in Glasgow doing formal metametatheory. My battlestar is not fully operational, but not far off...
I spend my life thinking about what to prove, not how to prove it.
A thing I've unlearned in my life as a dependent type theorist is that the context should be left-nested, with the type of each thing depending only on the values of things bound previously.
Yes, that's what happens, but it isn't important.
What's important is that each variable in scope at its use site has a type that's in scope at its use site. Which is a much weaker condition, implied by what tends to happen but not vice versa.
Conor Mc Bride
boosted
• Legislation which has been consulted on thoroughly, drafted carefully and subjected to parliamentary scrutiny is dismissed as rushed, ill-considered and undemocratic.
• The argument is made that other concerns are more pressing and this law change wastes Parliament's time.
Conor Mc Bride
boosted
Here's where I think some striking similarities are:
• Changes which mean young people have more access to information and support are called "a danger to children".
• Baseless fearmongering unsupported by evidence or experts is is called "genuine concern by reasonable people".
Conor Mc Bride
boosted
"Reverse the decision to block the Gender Recognition Reform (Scotland) Bill" https://petition.parliament.uk/petitions/631561
(d/dd) Edward Woodward = {Eward Woodward, Edwar Woodward, Edward Wooward, Edward Woodwar}
Tory trough-snouts will not be withdrawn.
Conor Mc Bride
boosted
Transphobia in The Guardian
What a load of rubbish Sonia Sodha spouts in this article 😬
I don't think she knows anything about Scotland OR trans people but I'll clarify some points.
"It makes it more difficult to provide single-sex intimate care for disabled women."- HOW!? These 2 things aren't related. In fact its in the same paper today that women's care/rape crisis are closing because of "lack of funds"
Conor Mc Bride
boosted
The minister who put their name to this case was Penny Mordaunt. It shows just how chilling an effect the anti-trans moral panic has had since then that during last year's Tory leadership elections she was forced to disavow this rational view to try to win over the Tory faithful.
Conor Mc Bride
boosted
Folk may not realise this but in 2018 the UK Tory government consulted on plans to reform the GRA to demedicalise the process in line with international best practice - i.e. exactly what the GRR Bill does. They issued guidance on the impact reform would have on the Equality Act:
Please stop naming things after me. I'm trying to make it to 50.
Conor Mc Bride
boosted
Every Virtual Learning Environment expands until it has a bug ridden unusable half implemented spreadsheet for incorrectly computing final marks.
Conor Mc Bride
boosted
Whatever you think about the merits of the Gender Recognition Reform Bill, the suggestion gaining currency among some unionists that the Scottish Government only pursued this legislation in order to provoke a constitutional clash with the UK Government is laughably misguided.
Conor Mc Bride
boosted
“Compiling higher-order specifications to SMT solvers” slides and link paper: https://bentnib.org/posts/2023-01-17-higher-order-specs-to-smt.html
A last-minute-COVID-forced remote talk about type based analyses for checking and translating higher-order specifications to SMT solvers.
