mafribe

106 ms·

1. 721.▲
   Why Are Little Kids in Japan So Independent?(citylab.com)

   3 points by mafribe 11y ago|0 comments
2. 722.▲
   by mafribe 11y ago

   Thanks your your reply. Idris has ... is that not satisfactory? I'm not an expert in Idris, but I think effects are encapsulated / encoded somehow in Idris. I don't think full Idris a logic, only the pure sublanguage
3. 723.▲
   by mafribe 11y ago

   I have no doubt that we will eventually be programming in a dependently typed language, the only question is when. For the reasons I give in another posting in this thread (inability to extend dependent types beyond pure
4. 724.▲
   by mafribe 11y ago

   Significant verification projects always plan for verification and do verification in tandem. That may be the case, but the point is that dependently typed programming languages force you to verify every intermediate step,
5. 725.▲
   by mafribe 11y ago

   after a certain point the validation overhead of advanced type systems is just not worth it. But what makes you think you need dependent types to do full specification and verification of a program? Instead you could use program l
6. 726.▲
   by mafribe 11y ago

   Well by that logic ... if you meet short people all day, then you're short?
7. 727.▲
   by mafribe 11y ago

   Maybe. So what? Even bad musicians are better these days, because of improved music technology. In terms of recording, production, distribution, learning music you can do with a laptop today what Beethoven and James Brown couldn't dre
8. 728.▲
   by mafribe 11y ago

   There are so many musicians out there that aren't quite good enough. I disagree with you. There are more good enough artists than ever. Pop music orchestrates the transition from childhood to adulthood. It helps structure s
9. 729.▲
   by mafribe 11y ago

   I think the real reason is that Germany had working debit cards for a very long time already, there was simply no need for credit cards. Every bank and store was accepting every banks's debit card. Since the big international credit c
10. 730.▲
    by mafribe 11y ago

    That really depends on the specific bank. I've got a debit card from a Sparkasse with Chip+PIN and 2FA for online transaction for quite a few years.
11. 731.▲
    by mafribe 11y ago

    And many/most of the people they hire too.
12. 732.▲
    by mafribe 11y ago

    there's some anxiety that there would be a storm of foreign students at British universities if fees were dropped. The UK used to have a system where foreign (= non-EU) students pay significantly more than home-students.
13. 733.▲
    by mafribe 11y ago

    While it is clear that one's access to capital is an important consideration, the article is weak, because it overlooks several important points, some which have been mentioned here by others. I'll mention two that I haven't
14. 734.▲
    by mafribe 11y ago

    It's an exciting time to be working in programming languages: industry is finally taking formal work in verification seriously, mainstream languages have nice type-theoretic features (e.g. Scala) and older languages retrofit them, fina
15. 735.▲
    by mafribe 11y ago

    require the students to defend their work in a viva voce and a written final. Time & effort, primarily. Also equality is a problem. Academics are human too, and tend to have preferences regarding looks, sex, nationalities etc
16. 736.▲
    by mafribe 11y ago

    cheating on an exam I was talking about coursework and dissertations. Cheating on exams is harder, although not impossible (e.g. bathroom breaks). it was made abundantly clear We also make this abundantly clear. But when
17. 737.▲
    by mafribe 11y ago

    I know what it is like to cheat and not to cheat: I cheated like crazy in high-school in my weak subjects, but didn't cheat at all at university because I was the best student in the year so copying from others would have reduced my gr
18. 738.▲
    by mafribe 11y ago

    the university is indirectly cheating when they publish statistics about the grades their students get. Not really as long as they don't guarantee that grade X guarantees a specific skill level. Clearly there is a usable corr
19. 739.▲
    by mafribe 11y ago

    Honor codes work As a working university teacher, I have to disagree with this somewhat. Cheating happens of a massive scale, I'd say at least 1/3 of all coursework I have graded involved some degree of cheating, and I&
20. 740.▲
    by mafribe 11y ago

    But is it always clear that the community sees as "proper [...] standards of behavior" is actually a proper standard of behaviour, or the sign of a dysfunctional community?
21. 741.▲
    by mafribe 11y ago

    I mean something simpler, and doesn't involve retargetting GHC. Write a Frege-to-Haskell compiler F2H, and then for each test T you simply compare the output of running Frege( T ) with the output of running GHC( F2H( T ) ). Maybe you h
22. 742.▲
    by mafribe 11y ago

    I should have read the InfoQ article more carefully. If you had a Frege -> Haskell translator, which shouldn't be hard to do, except in edge cases, you could use GHC as a testing oracle for the Frege compiler.
23. 743.▲
    by mafribe 11y ago

    How is the Frege compiler written? Is it a new compiler, built from scratch, or does it borrow heavily from a Haskell compiler?
24. 744.▲
    by mafribe 11y ago

    Yes, that's what I had in mind. If only there was an effect system that could guarantee purity and at the same time not be in the way (i.e. allow full or Scala-like type inference). Then purity would be guaranteed by types, like it is
25. 745.▲
    by mafribe 11y ago

    Thanks, that's a nice quote. I had read that text as a student, but overlooked this morsel. I wonder if Frege's older Begriffsschrift (1879) doesn't already discuss, or at least mention, higher-order functions. After all, i
26. 746.▲
    by mafribe 11y ago

    In what sense did Frege invent higher-order functions?
27. 747.▲
    by mafribe 11y ago

    Thanks. It's great to have basically Haskell on the JVM. I'll give it a try.
28. 748.▲
    by mafribe 11y ago

    Thanks. Type inference for types of rank > 2 is undecidable, how does this go together with the claim that Frege has type inference? I'm not a Haskell expert, but I think the {-# LANGUAGE RankNTypes #-} extension enables H
29. 749.▲
    by mafribe 11y ago

    This is a very good question. Continuations can be used to explain a wide variety of program control such as calling/returning (procedures), raising/handling (exceptions), jumping/labeling (goto and labels), process switch
30. 750.▲
    by mafribe 11y ago

    I think how a continuation is represented is an implementation detail that depends on many things, one of them being the ambient programming language and typing system (which may enforce e.g. linear usage of continuation). But in all cases