alcidesfonseca (u/alcidesfonseca)

alcidesfonseca commented on Typechecking is undecideable when 'type' is a type (1989) [pdf] dspace.mit.edu/bitstream/... · Posted by u/birdculture

IshKebab · a month ago

I haven't read this, and I'm not a type theorist so this is kind of over my head, but my understanding is that you can have decidable dependent types if you add some constraints - see Liquid types (terrible name).

https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li...

alcidesfonseca · a month ago

Liquid Types are more limited than "full dependent types" like Lean, Rocq, Agda or Idris. In Liquid Types you can refine your base types (Int, Bool), but you cannot refine all types. For instance, you cannot refine the function (a:Int | a > 0) -> {x:Int | x > a}. Functions are types, but are not refinable.

These restrictions make it possible to send the sub typing check to an SMT solver, and get the result in a reasonable amount of time.

alcidesfonseca commented on Typechecking is undecideable when 'type' is a type (1989) [pdf] dspace.mit.edu/bitstream/... · Posted by u/birdculture

TazeTSchnitzel · a month ago

This must be why kinds (types of types) in Haskell are a separate and less powerful thing than ordinary types?

alcidesfonseca · a month ago

I believe it to be historically true, but Dependent Haskell might change this (https://ghc.serokell.io/dh see unification of types and kinds).

In Lean (and I believe Rocq as well), the Type of Int is Type 0, the type of Type 0 is Type 1, and so on (called universes).

They all come from this restriction.

alcidesfonseca commented on Racket v9.0 blog.racket-lang.org/2025... · Posted by u/Fice

epolanski · a month ago

And all of them agrees to never use it after university, which is quite telling.

alcidesfonseca · a month ago

If it taught them the core concepts of writing good software, that's a win in my book.

alcidesfonseca commented on M4 Mac mini's efficiency jeffgeerling.com/blog/202... · Posted by u/marinesebastian

AcerbicZero · a year ago

Hah, Tim Cook decision pretty much sums it up; its the kind of thing that wouldn't have lasted 5 seconds when placed in front of Jobs (although there is a strong chance Jobs would have demanded his own nonsensical addition/subtraction to the design).

alcidesfonseca · a year ago

Jobs would have kept the button on the bottom, as it's not the proper way to use a computer.

Instead, he would have put motion/light sensors on the screen, so it would automatically wake up when you are sitting in front of it. Macs don't shutdown, they just go to sleep and wake up when you need them.

alcidesfonseca commented on Bend: a high-level language that runs on GPUs (via HVM2) github.com/HigherOrderCO/... · Posted by u/LightMachine

LightMachine · 2 years ago

Thanks, and I apologize if I got defensive, it is just that I put so much effort on being truthful, double-checking, putting disclaimers everywhere about every possible misinterpretation. Hell this is behind install instructions:

> our code gen is still on its infancy, and is nowhere as mature as SOTA compilers like GCC and GHC

Yet people still misinterpret. It is frustrating because I don't know what I could've done better

alcidesfonseca · 2 years ago

I think the (hidden) reasoning is that it is really easy to have speedups with slow interpreters. However, getting speedups in high-performance level programs is quite hard, mainly due to micro-optimisations.

That's where the comparison to Python comes from: getting speedup on slow interpreters is not very _relevant_. Now if your interpreter has the same optimisations as Python (or v8 or JVM), even a small fraction of what you show would be impressive.

Having said this, the work your team did is a really challenging engineering feat (and with lot more potential). But I do not believe the current speedups will hold if the interpreter/compilers have the level of optimisation that exist in other languages. And while you do not claim it, people expect that.

alcidesfonseca commented on Shoes makes building little graphical programs for Mac, Windows, Linux simple shoesrb.com/... · Posted by u/johnchristopher

douchescript · 2 years ago

I do like ruby a lot but I never grokked what was so great about _why, even though I coded ruby when he was active. Felt like a cargo cult. Maybe it was the depressive vibe of his stuff.

alcidesfonseca · 2 years ago

He was a poet who could code. Not a software engineer.

(disclaimer: I really like most of his ruby stuff)

alcidesfonseca commented on System memory allocator free operation zeroes out deallocated blocks in iOS 16 mjtsai.com/blog/2022/09/2... · Posted by u/ingve

alcidesfonseca · 3 years ago

Is there any way of measuring how many apps were affected by this change?

alcidesfonseca commented on I Miss RSS wilcosky.com/d/20-i-miss-... · Posted by u/behnamoh

timw4mail · 4 years ago

I follow Hacker News through RSS, as well as most webcomics that I follow.

There is one webcomic I enjoy, but can't get an RSS feed, because it's on a service similar to WebToons.

alcidesfonseca · 4 years ago

I am looking for more webcomics. Any that you'd recommend to others?

I mostly follow Dilbert and Questionable Content. I used to follow Wizard of Id and a few more, but they also lost support for RSS.

alcidesfonseca commented on Getting a Computer Science PhD in the USA parentheticallyspeaking.o... · Posted by u/azhenley

0xfaded · 4 years ago

Are there European universities that don't require a masters degree to start a phd?

alcidesfonseca · 4 years ago

In Portugal it is usually expected that you have one, but every now and then we accept a student without one.

Also notice that in Europe you can get a bachelor and masters in 4-5 years (3+1 or 2), which can be the length of a US undergrad degree.