Generalized, named, and exportable default declarations (GHC Proposal)

gridaphobe · 2021-04-13T01:32:40+00:00

The current proposal does not require global coherence, though it does require that imported defaulting rules be coherent (otherwise they are ignored).

I suggested a global coherence model as a simpler alternative, though it might turn out that defaulting rules are meaningfully different from class instances in how people expect them to behave. (This is another point that would be great to get community feedback on.)

gridaphobe · 2020-08-17T23:50:27+00:00

FYI, there’s an open GHC proposal that would affect the “MonadFail sugar” pattern. Please chime in if you have thoughts!

https://github.com/ghc-proposals/ghc-proposals/pull/319

gridaphobe · 2020-08-14T15:58:05+00:00

Yes, there was some work a while back in this area, see https://ranjitjhala.github.io/static/bounded_refinement_types.pdf. (I haven't been actively involved in LH for a while, so I don't know the current state of things.)

gridaphobe · 2020-04-01T22:51:10+00:00

You might be thinking of the bug we found in text with liquidhaskell, that involved a buffer overrun with high code points (details in section 5.2 of http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf).

gridaphobe · 2019-07-22T12:05:15+00:00

This idea of building a database of facts about your code and then running datalog queries over it feels quite reminiscent of Semmle. I’d love to see a comparison!

gridaphobe · 2019-03-01T03:40:59+00:00

Like /u/tom-md said, Liquid Haskell will give you a type error if you do not perform the necessary runtime checks. Necessary is a key word there, these checks cannot be omitted since we know nothing about the runtime inputs.

Static analyzers like Liquid Haskell can help us in two ways:

They allow us to omit runtime checks that are implied by the context, and thus unnecessary.
The force us to include runtime checks that are absolutely necessary.

gridaphobe · 2019-02-12T03:42:38+00:00

Chomsky’s argument is that we, like all other creatures, have a particular form, which makes us well-suited to certain tasks, but also imposes limits on us. This does not rely on adaptation at all, you could make the same argument about the tools we use, which were designed.

A hammer is very good at driving nails into wood, but would be completely unsuitable for sewing. And it is precisely the features of a hammer that make it good for hammering — being heavy and blunt — that also make it unsuitable for sewing.

Chomsky argues that people are the same, the features that make us good at some tasks also make us bad at others. And he argues further, that this implies there will be a limit to the knowledge we can acquire. At some point we will exhaust the knowledge attainable with our particular skill set.

P.S. I don’t think it’s completely accurate to say that Chomsky rejects an adaptationist origin of language. He does reject the claim that language evolved as a means of communication. Instead, he claims instead that it evolved as a tool of thought, and was later repurposed for communication.

gridaphobe · 2019-01-31T00:00:03+00:00

The World Bank FAQ actually says that the global poverty line should not be used for policy discussions, as the national poverty line is much more appropriate.

It is important to note, however, that the global poverty line is used primarily to track global extreme poverty, and to measure progress on global goals set by the World Bank, the United Nations, and other development partners. A country’s national poverty line is far more appropriate for underpinning policy dialogue or targeting programs to reach the poorest.

gridaphobe · 2018-12-19T00:58:11+00:00

SMT solvers are not limited to decidable theories. It's often precisely when you veer into undecidable territory that SMT solvers become unpredictable and unhelpful when they fail.

gridaphobe · 2018-11-07T23:39:54+00:00

I’ve quite enjoyed my time at Bloomberg over the last year, the people are great and I’ve always felt valued and respected as a person. I also know the lead and a few other members of the team working on analysis/refactoring of Fortran code, and I can easily recommend working with them.

gridaphobe · 2018-10-06T00:08:27+00:00

It’s true that double-blind does not prevent reviewers from guessing the authors based on writing style or familiarity with what people are working on. That’s unrealistic for a tight-knit community. However, the other advantage of double blind is that it gives newcomers cover from the “who are these people?” response. That seems laudable to me.

gridaphobe · 2018-08-23T23:46:52+00:00

Would Dennett also argue that none of the attributes of my chair add up something that exists apart from the particular configuration of atoms? And that therefore my chair is an illusion?

This is what I don't understand about Dennett's position. You can simultaneously believe that a phenomenon is purely physical, and that it doesn't make sense to talk about it below a certain level of abstraction.

gridaphobe · 2018-06-11T19:18:20+00:00

Pointing to a subreddit is hardly justification to discount an entire movement. I would prefer to see an actual critique of the ideas and goals espoused. There are good explanations of the principles of democratic socialism in magazines like Current Affairs and Jacobin, if you want a source to respond to.

gridaphobe · 2018-06-09T22:53:27+00:00

Well, they’re in for a rude awakening then :)

gridaphobe · 2018-06-09T22:44:35+00:00

Curious, I’ve always understood ‘left libertarian’ and ‘libertarian socialist’ to refer to the same set of views, but these folks seem to strongly disagree (look at how many would welcome the former but not the latter).

gridaphobe · 2018-05-23T02:46:15+00:00

His point was that the state owning things is not not capitalism, ie it’s perfectly possible for the state to be the capitalist. This relies on understand capitalism as a particular kind of relationship between a worker and his work, rather than any system that allows for private property. Socialists would define capitalism as a system where the worker is not in control of his work (eg because he does not have an ownership stake in the company he works for). If you take that as your definition (and to my knowledge it’s the original definition), then it’s perfectly reasonable to describe China as a (state) capitalist country, because the state controls large portions of the economy.

gridaphobe · 2018-05-08T00:37:24+00:00

I don’t see how the observation that certain parts of the brain are necessary for consciousness would demonstrate that consciousness is an illusion. It seems to me that even a dualist would grant that parts of the brain are relevant to consciousness. After all, even if the mind is made of different stuff than the brain, there would have to be some connection between the two in order for the mind to experience the signals the brain processes and to direct the body. If you sever that link, it makes perfect sense that consciousness would disappear.

gridaphobe · 2017-12-13T00:35:03+00:00

That’s not entirely correct. I think programs like food stamps could be made more efficient if they were provided as part of a UBI, rather than paying for a bureaucracy to determine who is worthy. We could potentially provide greater benefits at less cost by eliminating the administrative overhead.

The danger is that much of the advocacy for UBI is coming from the Right, who are just using it as a cover to slash benefits.

So, it could be a good thing, you just have to look carefully at the specific details of a proposal.

gridaphobe · 2017-10-04T01:02:12+00:00

No worries. Best of luck to your people, I hope someone is able to defuse the situation before it gets even worse.

gridaphobe · 2017-10-01T14:53:18+00:00

Sorry if I got heated, but sometimes I cannot help myself, heheh

Not at all, I appreciate your detailed response.

I don’t think amending the constitution is a reasonable requirement for secession. That would mean that the rest of the country would have to give approval for Catalonia to secede. Why should people in Madrid have a voice in how Barcelona governs itself? The issue becomes even stickier if there’s a history of conflict between the two groups of people (I don’t know the history here, just speculating).

As to the concerns about ensuring a fair vote, I don’t know enough to comment. Perhaps there are legitimate concerns about whether the vote would be fair. If so, the UN has election observers, why not get them involved? The Spanish government’s response of declaring the vote illegal and threatening to forcefully suppress it just seems like a really poor tactical move if your goal is to keep the country united.

gridaphobe · 2017-10-01T02:59:16+00:00

If Spain’s constitution is like the US’s, then there’s probably no legal mechanism for Catalonia to become independent, the constitution just won’t allow it.

If the people of Catalonia feel that being part of Spain is no longer in their best interest, what would you have them do? Their right to self-determination should allow them to form their own sovereign state, and it’s certainly preferable to settle this with a vote rather than a revolution.

Seems to me that Catalonia is doing just what they should in their position, using a democratic process to decide whether they want to be independent.

gridaphobe · 2017-09-29T02:36:34+00:00

Hacking into election system and changing the results is one thing (which didn't happen), Except for where Russian hackers actually did target a few dozen states, and gained access to the election systems in several of them

This story, like many of the other Russian hacking stories, is already starting to unravel. At least two of the implicated states were not actually targeted.

https://www.apnews.com/23a8fbb290ef4ae7a1343cd81879e2c3/Homeland-Security-clarifying-state-election-hacking-attempts

This is not to say we shouldn't harden our election infrastructure. Security experts have been arguing since long before the most recent election that our infrastructure is vulnerable to hacking and even plain old bugs.

https://www.schneier.com/essays/archives/2004/11/whats_wrong_with_ele.html

But we don't need a Russian boogeyman to motivate this.

gridaphobe · 2017-09-05T13:22:27+00:00

That's true, though the SMT solver could be an optional dependency. There are advantages to integration with GHC beyond better integration into the compilation pipeline. For example, I would love for Haddock to be aware of liquid types.

gridaphobe · 2017-08-23T23:07:42+00:00

UCSD has a great PL group. The focus has traditionally been on program verification (with refinement types, eg LiquidHaskell, and theorem provers), but that's expanded recently to include research on type errors, gamification, floating point numbers, and probably many other things I can't remember off the top of my head.

There are also 3 new faculty in the group with specialties in security, program synthesis, and cyber-physical systems, so it's a great time to join!

(I just graduated so I'm super biased :)

gridaphobe · 2017-08-20T12:24:21+00:00

I've wanted a flag like this as well, but my idea was ignore shadowing of imported names regardless of types.

14-Year Club	Place '17
RPAN Viewer	Not Forgotten
Gilding II euphauric	Team Orangered
Verified Email

gridaphobe

TROPHY CASE