Hacker News new | past | comments | ask | show | jobs | submit | lang_agnostic's comments login

Isn't this just phantom types in other programming languages?


More like `newtype` with implicit `coerce`


> We are now moving away from auto-focus and auto shutter speeds toward on-the-fly retouching, editing, of material by the camera

This is a great point but it's not what the article is about. This is about bringing existing features of digital cinema cameras to a portable phone.


Yup. And the move from a camera to a cinema camera incorporating cinematography trickery represents a marked change in what a personal camera is and does.


This isn't any trickery, this is a file format. One that actually avoid the uncontrollable computational photography done by default and actually changes the nature of the picture without the input of the user. This is helping conserve what we think of pictures as a digital capture of light. Rather than what it's becoming, which is the product of hallucinated details by a neural network.


Is this person actually asking for Monads and Higher Kinded Types?

It would solve the problem they're raising but somehow I suspect that's now the solution they want to hear. And also the rust version would be quite hard to use due to the memory management model.


I think the author wants something like Ruby's blocks, although you're correct that monads would also be a good fit.

In Ruby, iteration can be performed by passing a sort-of-closure called a block. Unlike passing a closure (function), returning early from a block acts like returning from a for loop.

If a language has a garbage collector and no user-visible separation between stack and heap allocation, then there's lots of interesting things that language can do in terms of building "fluent" APIs.


In my experience, when it comes to language design, most people end up wanting monads and HKTs but refuse to admit it / are scared of admitting it.


This asking GPT for inference needs to stop immediately before it becomes accepted and commonplace. This is almost the same as "I flipped a coin and the gods spoke to me"


It's far worse, because people who should know better, people who should understand at least the very basics of how the underlying algorithm works, are deluding themselves into believing it's some kind of magical oracle.


It really isn't that far removed from the "anonymous sources" journalists cite or the slander levied on political undesirables at Wikipedia.


Tangentially, I think there is essentially already the beginnings of a cult of AI, based around the promise of technological salvation from worldly toil with somewhat eschatological undertones.

Just waiting for "Show HN: Repent, sell your house and car, invest everything into eternal-salvation.ai before it's too late and you're left in the dust as we ascend to the stars!"


I'm quite surprised but how large and extensive this guide is.

As someone who learned to drive in Europe I've always been extremely confused by the signage and road layout of American roads. There is a pretty big difference in quality between state roads and federal roads. The former seem to have no coherent style, layout or identity while the latter seem pretty consistent. Given the above documents I can see there is a consistent style but the style does not seem to translate to a consistent user experience.

The three things that stand out to me are the amount of text on each sign, the lack of standardized rule about entries and exists, and the lack of road markings, specially at intersections.

The first one isn't necessarily a big problem but it's very weird to have all this text when you could have instead a very recognizable sign that you can understand from afar (the one way sign is a great example), instead of a white sign with black text that you can only read once you're close to it and only understand if you know English.

The second one makes highway layout extremely confusing and, at least for me, feel dangerous and stressful. Some Signs can tell you to take an exit with make 20m of notice and it's a 90° right turn and you also need to go from 120 kmph to 30 in that span. The reduced speed sign is only visible after you've turned so if you dont know the area you're almost always going too fast. Because it's a 90° turn with trees in the sides you can't anticipate what the traffic is like after the turn. If you know the area you probably have no problem handling this situation, but driving there for the first time feels like driving through a minefield. There are other instances of this with left exits, overtaking from both sides, turn right on red, stop sights everywhere, no priority system, and more.

The last one is incredibly frustrating when you come from Europe because over there, most intersections have redundant signage and markings. Intersections have street lights that tell you where to go, the road layout is advertised on a sign well in advance, and the paint on the road tells you how to turn and where to stop and even indicates speed limits or directions. Intersections in americas provide no such affordances. Intersections are basically a free for all between the incoming trafic, the people turning right on red and the pedestrians. I was expecting a lot more from a country which is built for cars.

It feels like roads are built for cars but not for drivers.


>Some Signs can tell you to take an exit with make 20m of notice and it's a 90° right turn and you also need to go from 120 kmph to 30 in that span.

There should be a sign for this situation, for example:

https://www.google.com/maps/@47.6277564,-122.3289325,3a,73.1...

Also FWIW: https://mutcd.fhwa.dot.gov/htm/2009/part2/part2c.htm#table2C...

Europe does tend to have better signage in intersections. But the concept of a national speed limit and then not marking the speed limit when it's in effect seems brain dead. How are you supposed to know what it is if say you just rented a car from the airport?

The other thing that kills me is not using a different color for separating lanes that run in the same direction vs different directions (white vs yellow in the US) How do you know at a glance if a road is one way?


> But the concept of a national speed limit and then not marking the speed limit when it's in effect seems brain dead.

Yeah. Have you driven in France? On regular roads, there's no "national speed limit". Depending on the department, it can be 80 or 90 km/h.

> How are you supposed to know what it is if say you just rented a car from the airport?

Nul ne doit ignorer la loi (no one may be ignorant of the law).

> How do you know at a glance if a road is one way?

If there are only two lanes, you look at the line on the left border of the road. If the line is continuous, both lanes go the same way. If it's dashed or there's no line (and your side doesn't have one either) you're on a two-way road.

If there are multiple lanes, there will be a double continuous line separating the ways. The double line can sometimes appear on two-lane roads, it always means the road is two-way.

Yellow markings exist, they usually mean road-work / temporary signaling.

Best rule of thumb: if you're not clearly on a highway, it's very likely a two-way road. Clearly means there's no other separate set of lanes close by. We don't have as much space as in the US where the lanes going the other way are so far away you can barely see them.


> Nul ne doit ignorer la loi (no one may be ignorant of the law).

I got a parking ticket once in a place that had parking signs and a parking meter. Turned out that particular parking meter was only for cars with a specific permit. How could I have known that? Because there was supposed to be a painted 1" green circle around its base. Even if I had known what that meant, the circle had worn away probably years prior. No, there was no mention of these circles or their meaning on any of the parking signs.


Urban street parking in particular can have really confusing signage with all sorts of conditions and exceptions. And, especially where parking is really tight, I often find that I feel I'm missing something if there's actually an open space.


>Nul ne doit ignorer la loi (no one may be ignorant of the law).

Sure, but humans aren't clairvoyant. You can make the effort to look it up, or the road authority can just put up some basic signs.


I agree with you, but that's how things work over here.

To stay on the topic of speed limits, there's a national speed limit for towns / cities, 50 kmph. It's usually not posted as such, but there being a sign with a town name means you must observe that.

Other peculiarities you have to know: when you enter a town, there may be a different speed limit posted than the national limit, typically 30 kmph, very rarely 70. It matters if the speed limit sign is physically attached to the name sign, or if it stands on its own. In the former case, it means that's the speed limit for all the streets of the town. If not, it's the regular limit, meaning until the first intersection, when the default one comes in effect.

The signs are otherwise identical.


While (as a European) I agree with your point regarding speed signs, I think an important point is that there are plenty of traffic laws that differs (even) between EU countries. So when going driving in a foreign country one really should look up at least basic rules beforehand, and speed limits will most likely be front and center.


Note that if you cross a border in Europe (not necessarily in the EU) by car, you will pass a sign [0] giving the default speed limits for each type of road.

[0]https://commons.wikimedia.org/wiki/File:National_speed_limit...


> The other thing that kills me is not using a different color for separating lanes that run in the same direction vs different directions (white vs yellow in the US) How do you know at a glance if a road is one way?

I agree completely, I've lived with it all my life and I don't understand it either. How you know? You don't, always. When in doubt, keep right.

50 years ago my dad had an accident precisely on account of this. He got confused about what stretch of road he was on, changed lanes into oncoming traffic, and hit a truck head on.

Good thing he was driving a Volvo. He bruised his knee.


In Europe, the lane to your left is in principle always oncoming traffic, unless you see a separate road to your left with a bit of grass in between. Or at least there will be a continuous instead of a dashed line.


That means you have to look in two places, correlate the information and make a deduction. I would prefer a style of line that is immediately recognisable on its own.


It's simpler than that, one can only change lanes when they are separated by a dashed line. Solid lines you are not supposed to cross.


Well, there are bidirectional roads with dashed lines in the middle, so you can overtake, but you should obviously not stay in the lane with oncoming traffic for longer than that. I can see how colours can help there, but in Europe the road situation tends to be clear enough that that isn't necessary.


I've always seen national speed limit signs at the exit of airports, similar to the signs you see at national borders. Here's the one at the exit of Schiphol: https://goo.gl/maps/PD6jvvpsDgV3Rwq97


>But the concept of a national speed limit and then not marking the speed limit when it's in effect seems brain dead. How are you supposed to know what it is if say you just rented a car from the airport?

By learning the traffic rules before you rent a car, how else would you know what else is different than what you are used to?

Not marking the national default speed limit is done to limit the amount of signs


> https://www.google.com/maps/@47.6277564,-122.3289325,3a,73.1...

I wonder if the MUTCD has a section on keeping the graffiti consistent nationally as well.


Turning right on red is the one thing I'll defend here. You can only turn right on red after coming to a complete stop, and you have to yield to any traffic (including pedestrian traffic) before you make the turn. Given those restrictions, it's strictly an improvement as far as traffic flow is concerned.

Totally agree with you on exits though, especially left exits. Since moving to Texas I've become a big fan of frontage roads, but not everyplace has the room for that.


I'd be happy if people even stopped at STOP signs - the number of idiots who think the law doesn't apply to them at the STOP signs around our way is stunning. A kid was killed a year or so back because some teenager blew through the intersection without checking.

As for right-on-red, I think (as a Brit) it's awesome, but I don't think I've ever seen a single person come to a complete stop before going right, in the 20 years I've lived here. At best, it's slow-down-while-I-check.


Also, right on red means those drivers are so preoccupied with looking left to see if traffic is clear they never even glance to their right until after they have completed their turn and are accelerating. Non-automobile users beware.


Those are some of the most routinely and carelessly broken of all driving rules, which is really saying something. Being a pedestrian in a large city that allows right on red is scary as shit, I've had more close calls that way than everything else combined. The only thing that comes close is uncontrolled crosswalks across four lanes. Which also should not exist.


Frontage roads are quite useful, but the near-complete lack of cloverleaf ramps in Texas is maddening. You can't just smoothly flow from a freeway to a surface street, which means you're always having to hit traffic signals. 610 at Westheimer in Houston is a perfect example of all that going completely wrong.


You simultaneously make a great and stupid point. The stupid part is obvious: operations are allowed because writing programs is useful. Now for the great, nuanced and complicated point: How do we detect errors when manipulating floats while allowing us to write the useful programs?

This boils down to two things: 1. What do we think is correct at any given time for any given program? The compiler can't know so we have to tell it, which brings us to 2 2. How do we write down in our programming language what is supposed to be correct?

The problem with floats is that sometimes you care about precision, sometimes you don't sometimes you care about overflows, sometimes you don't. Sometimes you care about inverse operations, sometimes you don't. Commercial programming language which only expose a "float" types usually are unable to deal with the greater complexity of _ensuring_ that some property you care about isn't broken. That is why compilers let you operate on floats and shoot yourself in the foot when you divide and then multiply back.

On the other hand, one could imagine a future programming language (and some academic experiments already exist) where you can tell the computer "in this part of the code, it's important that I never overflow" or "in this function, I expect multiplication and division to be inverses of each other". In which case the compiler will display diagnostic information if you do something that break those properties.

It's not clear yet what is the most convenient user interface to write down and check those properties. But many believe it by using even more advanced type systems than Rust. Many other believe that we can add static analysis atop existing programming languages to obtain the same result.

TLDR: Rust allows it for now because 50-100years in the future we'll have to tools to tell when it's ok and when it's not ok to multiply floats together. Right now we're still smacking rocks together to make fire.


Tokens of recognition aren't currency that you can use to buy redemption, I find this comment particularly ironic when this other article exists, perfectly capturing a symptom of the state of denial that the US find themselves in wrt to their tumultuous history: https://news.ycombinator.com/item?id=30261610

Germany didn't get over their trauma by having "Jew day" and "please stop treating humans like cattle" bill while routinely allowing their members of society to deny education to their children


I think the school system is a failure for many blacks, but they aren't denied an education. I think we need a system where black parents can send their kids to a better school than their local school.

The problem is this is not a black problem, but a poor problem. Poor areas, regardless of their racial makeup, have worse schools. This has nothing to do with race, but class.

I agree that just giving a day or month or whatever doesn't solve the issue, but when the people involved are all dead, we can't exactly hold a Nuremberg Trial equivalent. We also have a first amendment so we can't ban racism like Germany did with Holocaust denial.


The evidentiary standards used at Nuernberg would be problematic in the US today.

Poor Whites and Asians still have better outcomes than similarly poor Blacks.


Woman are now doing better in school than men. Does that mean that the school system is sexist against boys?


School haa been remade and reprioritizatized to enable women to perform better.


Hi there,

I'm a phd student working on Idris and I used to work with Edwin on this, if you want more info or want to see more practical applications of idris2, Dependent types, or QTT, here are a couple links:

- idris2 is written in idris2 so that's a good example of a big program using dependent types https://github.com/idris-lang/Idris2

- we have some very interesting libraries in the works: https://github.com/idris-lang/Idris2/wiki/Libraries

- my own projects in idris include a purely declarative server library where you give the API and the server is completely implemented and instantiated from your description https://gitlab.com/avidela/recombine


I'm curious if you have any insight into what a realistic lower limit to Idris compile time speed looks like. Right now even moderately sized Idris programs can be quite slow to compile, slower than even other dependently-typed languages (see e.g. https://github.com/AndrasKovacs/smalltt). How much of this is intrinsic to Idris' language design and how much of it is due to lack of optimization in the implementation?


I reckon we can get the raw performance quite low, but it might be a challenging environment to program in, the ergonomics of programming linear types aren't figured out and it would involve a lot of memory management. While safe, reasoning about memory can be quite hard, just like anyone learning how to handle the borrow checked in rust can tell you.

It's currently one of my project to use QTT to statically enforce performance invariants and optimisations, currently I am looking at partial evaluation of programs and explicit annotations to control which parts need to be partially evaluated and which parts need to remain Unevaluated.

Regarding the benchmarks there are two things to address to make them go faster:

- the idris parser is actually pretty slow so we should get working on that

- the examples use explicit runtime bindings for type parameters which force the types to be allocated and available at runtime, which destroys the performance of some programs (stlc notably)

It's not expected to write idris code in that way since linearity annotations also allow you to _remove_ values from the runtime and make dependent programs go faster, if you were to be concerned about runtime performance you would use _runtime erased_ type variables instead of _runtime relevant_ variables. Some of this is due to the foreign nature of QTT, and we should do a better job at teaching how to use it for performance.

On the other hand someone could argue "if idris is that smart can't it warn/perform those optimisations automatically?" And maybe that's the way to go, but we need more eyes and brain looking at the problem and coming up with prototype solutions to make progress. idris is still a small project so we don't have enough people working on it to implement those smart features


I might have misunderstood both comments, but I have the impression the OP was asking about speed of compilation and you're mostly talking about the performance of the compiled code?


I need my answer was focused on runtime performance, thanks for pointing it out. However, They are related for two reasons:

- idris is written in idris so any improvement in the language results in faster compile-times, if more things are annotated with 0 in the compiler, thing will compile faster.

- if some variable is only important at compile-time, the compiler doesn't have to look at it with very much scrutiny. That saves you a lot of time when typechecking


> if some variable is only important at compile-time, the compiler doesn't have to look at it with very much scrutiny. That saves you a lot of time when typechecking

Right, but if some code is annotated with unrestricted multiplicity, but still not actually used anywhere in a function body, does this make compilation of that code slower than if that same code was annotated with zero multiplicity?


Oh fascinating. Are you saying that multiplicity annotations can affect compile time speed (in particular giving a laxer multiplicity than what is required)?


Yes. Multiplicity 0 removes the value from the runtime avoiding allocations and garbage collection. That particularly handy for type-level indices and type-level programs in general.

Technically speaking multiplicity 1 (linear variable) can be subject to arbitrary inclining though it's not implemented in the compiler.

I'm working on other multiplicities that could allow you to describe which values are "compile-time" available, and therefore subject to optimisations


> Multiplicity 0 removes the value from the runtime avoiding allocations and garbage collection.

Does this apply even for compile-time evaluation? I'm not sure of the specifics of how Idris does compile-time evaluation vs runtime evaluation.


Education?


Students cheapskates unless they're forced to buy something by the school.


No mention to earthquake or typhoons?

I always thought the urbanization of Japan was mostly limited by natural conditions.

Indeed, there is no point in making tall buildings if they are more likely to fall and cost more in repairs and anti-seismic technology


San Fransisco was one of the main cities Tokyo was compared to, which faces very similar natural conditions.


There are definitely lot of policy, infrastructure, and cultural differences in play as well, but this is a huge factor the author missed.

Japan didn't allow any tall buildings until 1963, so the development of tall urban centers came very late, and as others have mentioned, followed patterns of existing rail infrastructure.


Yeah, that was an obvious omission.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: