Looks like I just had to click a thing to do the first one. Nice! :blobhappy:
@abs Here's what I alluded to earlier about record projections (which makes the first naive attempt in your post typecheck) https://gist.github.com/Lysxia/1ee6f3371536e1a00a9c3788faa7e6f1
I've set up my blog (with one post!).
You can find it here: https://no-learns.neocities.org/
satania.space seems to be broken right now, so I'll be hanging out over here until @satanya comes back to fix it.
If you haven't noticed it yet, I have been posting pretty much exclusively over at @abs for a while now. I'm gonna move over there fully now, so please follow me there if you want to keep up with my stuff.
#reintroductions coz why not:
hi i'm into #programming , trying to learn (more of) #idris rn, I used to do a lot of #blender #3d stuff, some 2d art but nothing worth uploading, i watch a bunch of #animation (when i can) aaand sometimes i run.
also interested in #teaching and how it relates to the #hacking mindset.
oh and i like #plan9 (the operating system) and learning about weird systems and languages and stuff
aand i use it/its pronouns.
He also seems to ignore dependent types in many of his later points of what types can't express, but I guess he just doesn't know about them? He doesn't seem too well versed in PLT.
I watched Maybe Not* this morning and I'm not sure what to make of it.
Some of the points (union types vs sum types) were really good, but a lot of stuff was at least badly put as well.
As I see it, he rags in type systems for a while and then contrasts that with contracts (without calling them that) and just conveniently ignores that the guarantees between them are wildly different. That seems somewhat underhanded tbh.
*: Maybe Not - Rich Hickey - https://www.youtube.com/watch?v=YR5WdGrpoug