So this creates the function code from the types? I don’t understand how that works.
If I have Int -> Int -> Int how would that know I want the function foo bar baz = bar + baz and not foo bar baz = bar - baz?
Int -> Int -> Int
foo bar baz = bar + baz
foo bar baz = bar - baz
It can’t. Your type is too general. Not sure what this specific plugin will do, but it will probably just come up with some expression that will have that type. Possibly the one you want – but probably not. :)
For example of types of functions where the types will only allow one, correct implementation, look up implementations of e.g. length-indexed vectors or red-black trees in dependently typed programming languages. It’s also interesting to look at the interactive modes for languages such as Agda and Idris where you can tell your editor “complete this expression” and it will do that (or tell you that it’s not able to, and what’s missing).
I think it is relying on the free theorems guaranteed by parametricity.
See Philip Wadler’s paper Theorems for Free!
I believe that these tools are not based on parametricity, merely on syntactic proof search (in essence, enumerating possible terms at this type, using techniques from the proof search literature). If you think about it, theorems-for-free does not actually help you generate code at arbitrary types.
But I think the fact that this is possible is a side effect of the free theorems granted by parametricity.
Which explains why it is not possible to do this with a concrete type signature, as per the original question.
Abstract types and parametric polymorphism are a nice language feature that has several consequences. One is the existence of free theorems (technically, a nice denotational semantics in the categoy of relations), another is the possibility of having a restricted enough search space that blind proof search produces sensible/interesting program. Those two consequences are independent, I don’t think that you can claim that one is a “side effect” of the other.
“Theorem for free” is an interesting and thought-provoking and well-written research article, so people will easily share it and think about it. This is great! But it also result in some miscomprehensions (or at least exaggerations) about what the result says, which result in the article sometimes being cited in situations where it is not actually relevant (besides being in the same scientific domain as the work being discussed). I thought you may be interested a slightly more detailed picture of the technical details at play here.
Thanks for the clarification. As you say, this is stuff I know exists, but do not work with it daily so do not understand the full implications and shortcomings.
I simply leave out the email address from the global gitconfig file (that’s synced between computers), and will be prompted by git to provide it the first time I want to commit for every new project I clone.
Seems to be fixed in macOS 10.13.2, too, with some refinements(?) coming in 10.13.3:
Both are far too complicated for me. As a smarter person than I once said, “any command I cannot immediately remember might as well not exist.”
typing tmux on a remote server beats having to restart a job when the network connection dies…
That use case fell away for me when I started using mosh.
Mosh is great, but it doesn’t solve the issue with client dying (e.g., due to logout or reboot) and doesn’t let you connect from multiple clients.
My question is why you would want to pretend that programs don’t modify or have state. That seems like attempting to do welding without heating metal. Hot metal can cause problems and requires skill, but it’s kind of the point.
I’m only talking for my self, of course, but I don’t pretend that programs don’t mutate state when I write code in a purely functional language. I know the compiler will do that behind the scenes. Having immutable state in the programming model is about eliminating some classes of bugs and making it easier to reason about.
I’m also really happy about having virtual memory even though I’m only “pretending” that I have large, contiguous blocks of memory in a suspiciously big memory space.
(Juggling [memory blocks] can cause problems and requires skill. ;)
Good point, but all abstractions are tradeoffs. Even virtual memory is an abstraction with a cost. There is a compelling argument in favor of being able to mark functions or calculation as side effect free or purely functional, but it seems to me that e.g. trying to make I/O “functional” involves a lot of effort and complexity and no real advantage.
This is an area of active research, so I don’t expect that monad transformer stacks are the last word in handling effects. That said, in order to mark something as “side effect free” or “pure” requires that you have a way of encoding what is impure. That is, you can’t just say: “This is a pure function!” without knowing what “pure” means. Monads and monad transformer stacks are essentially ways of saying: “This thing handles impurity of a particular kind.” For example, Maybe handles the impurity of a result that may or may not happen; Reader handles the impurity of a configuration environment; Either handles the impurity of two potential branches of execution (i.e. errors).
I’m restricting myself to “pure function” as “no side effects”. I have never understood the utility of monads - they seem to be complex ways of describing mundane operations.
That’s what I’m saying, though: a “side effect” has to be codified somehow. If it isn’t captured in the type, then it looks fine to the compiler; printf returns an int, after all, so how is it to be marked as a side effect? That is the utility of monads. Maybe (or Result in Rust) is the most obvious example: your type is literally saying “Something may or may not come back,” and you then must deal with that either by passing that uncertainty “up the chain” or by dealing with the uncertainty at the point of origin. This is encoding the side effect of an uncertain return which, in more typical languages, is represented by null (None, nil, …).
If your mechanism of capturing function semantics is restricted to the type or signature, you have to encode all sorts of things in the types. Alternatively, you could just have a keyword, as in D, for example. I’d like a compiler directive in C to designate a function as “pure” in that sense - it would allow many optimizations and perhaps discourage C compiler writers from coming up with stupid optimizations based on undefineds.
Ok, I didn’t know that GCC/Clang both support “pure” attributes. So there.
2bluesc on HN made a pricing/“spec” provider comparison gist.
… and someone else expanded it to include DigitalOcean, Vultr, Linode, OVH, and Scaleway:
I like typeclasses in Haskell, but I can totally see why Elm doesn’t have them due to its focus on being easy to learn (especially for people coming from js) and having good, helpful and specific error messages.
I really hope it’s possible to have good error messages also with type classes, but at least today, with GHC, they are very confusing for beginners. Since you could have a Num instance for strings, the error messages when beginners try to appending strings by using + is
No instance for (Num [Char]) arising from a use of ‘+’
expecting the argument to be a number, but it is a string
Using Vim is going to be interesting on one of these… I bet people will just remap the Caps Lock key as Escape or something similar. Still, I think the touch bar will be an overall improvement outside of the specific communities that required the old setup.
It’s always been really inefficient to pull your hand off the home row and reach way up to the escape key. Vi was designed for a keyboard that had the escape key where the tab key is in a US layout. Remapping capslock to escape or typing ctrl-[ has always been the pro-vim user’s way of generating an escape keycode directly.
I tend to map “jj” to escape. Works well, can be typed very quickly, and I doubt people type “jj” very much, if at all.
Yeah, that or use the ±§ key (top left, next to ‘1’ on UK keyboards) or it’s equivalent. I quite like using Caps Lock as Ctrl (and I’m a Vim user).
I’m curious to see what it’d be like to use the Esc on the touch bar - I’m guessing the feel will be too different to the rest of the keyboard for most people.
inoremap fd <ESC>
inoremap jj <ESC>
inoremap jk <ESC>
You’ll thank me later.
Using vim with the usual ESC location already sucks.
You can use ctrl-c instead of esc in vim.
You probably want to use ctrl-[. Ctrl-C will not trigger autocmds, abbreviations and so on.
zsh, mostly for this https://github.com/bitemyapp/dotfiles/blob/master/.zshrc#L14-L16
Care to explain what those lines do? :)
Don’t remember. Got ~200k elisp in my dotfiles plus other stuff. Have to use bash for a bit to remember. Think it has to do with making the completion less gormy.
I don’t really remember things since I started on the book a year and a half ago.
Is there a reason for using character entities instead of just inserting the characters themselves – apart from wanting to make it clear which one it is for characters that are displayed in the same way?
On a Mac, long known for its typography (Steve took a calligraphy class before dropping out of Reed College), it’s very easy to use the Shift and Option key modifiers to insert all sorts of characters, from mdash to the «angle quotes».
On Windows — not so much, so, things like — and «/» come in quite handy.
If the FBI had the ability to brute-force the device, what would the outcome be? I would hope (but doubt) Apple complying would make no real difference (i.e. brute-forcing would take decades) due to the security.
The phone in question is an iPhone 5C. It doesn’t have the secure enclave that later A7 models have, so the delay for wrong guesses is only in software. See http://blog.trailofbits.com/2016/02/17/apple-can-comply-with-the-fbi-court-order/ for a good summary.
In order to limit the risk of abuse, Apple can lock the customized version of iOS to only work on the specific recovered iPhone and perform all recovery on their own, without sharing the firmware image with the FBI.
Even if there were a way to tie it only to that specific device, they still have to create and sign a neutered version of iOS. I think the signing part gets into tricky 1st Amendment stuff.
Hmmm.. and, if the FBI were to attempt any reverse engineering, could Apple file suit under the DMCA? That would be amazing.
From 17 U.S. Code § 1201 (e):
This section does not prohibit any lawfully authorized investigative, protective, information security, or intelligence activity of an officer, agent, or employee of the United States[…]
Yes, I forgot about that. Shame.
I’m not a lawyer and this is not legal advice. :)
I can’t see how the 1st amendment would apply here. The only one which gives a right not to speak is the 5th, and Apple is not implicated criminally in this case.
E-reader friendly now too!
What does this mean, exactly? Is there an extra non-margin PDF, or is there actually an epub version available now?
I too hope to see an epub at a certain point. The ereader PDF has some code that overflows in the late chapters. It is much better for tablet reading however.
I’ve read this morning the Monad chapter and the functor/applicative/monad in the wild. They are really top class (as the rest of the book)! I look forward to buy also the paper version when it’s ready!
I too hope to see an epub at a certain point.
We’ve tested an epub render, it mangled the content horribly. I’d rather just fix the PDF via the LaTeX.
Glad you’re liking it so far :)
Boo, epub would really be a lot nicer for reading on a tablet beside the laptop. Curious what got mangled.
The e-reader version of the PDF I made vastly exceeded my expectations. I poked around it a fair bit on my kindle and it was very nice, IMO. Other readers that tested it on various devices gave it a thumbs up as well.
epub on my kindle was horrendous and the gaping maw of labor required to fix it by hand isn’t going to happen. I’d have to charge a lot more for the book to cover that and people already complain about the $59.
Ooh goody, I’ve been mostly reading it on my kobo so this is good. The book really has been great so far, things like the structure, you can find exercices sprinkled throughout the chapters instead of all globbed at the end, I usually have trouble getting into a books exercices because of this. They’re even little goodies at the end of chapters in the form of links to recommended extra reading.
there is an LED inside the case, so you can’t see it if you have your iPhone in there.
And you don’t need to since the charge status is displayed on the phone’s screen…
What does it mean to type like a madman? If I’m giving a presentation, I want to stop and talk between some of the commands, no? I don’t want the script to get too far ahead of me, but how does a madman prevent that from happening?
From the description (“replays the commands in a fake terminal session as you type random characters”) it sounds like you need to type in order for it to progress. I just doesn’t care what you type. So to stop and talk, simply stop typing. :)
I’m guessing it waits for enter between commands, but that’s really the part that’s not clear. Perhaps obvious, but the description would imply the opposite.
Having played with it a bit now, keys need to be pressed until the command has been typed out and then enter activates the command. If you set a speed ie -s 4 then it will print 4 characters per character of tapping on the keyboard - but an enter is required when you get to the end of the command.
I love the website design, did you do that as well?
both (app and site) look great. Congrats!
Thank you. Really happy to hear that! :)
Yep, I did the website design myself, using Scenery to create the images.
Looks great, congrats on the launch.
Thanks. I used an early version this summer (Spain, Gibraltar, Morocco) and it was very convenient. :)
Related: Am I the only who goes through headlines or titles that I’m copy-pasting and replaces every punctuation character with one output by my (US English) keyboard? I loathe the Unicode dash.
What’s wrong with the unicode dash?
Yeah, I’m a huge fan of the Unicode em dash—seen in use here—because doubling up en dashes--ew--feels broken up.
You’re probably not the only one, but out of curiosity: Why do you do it? Because you’re used to how it looks? Because you think it looks better?
I greatly prefer real dashes instead of double or triple hyphens and even use proper quotation marks and non-breaking spaces when writing.
Interestingly, I use real em dashes, en dashes and ellipses (“…”), but straight quotes and apostrophes. (Aside: lobste.rs automatically unstraightens quotes, which gives me a perverse urge to try to make it screw up.) I can easily type the dashes and ellipsis with compose key combinations, but not directional quotes (though «guillemets» are possible), which may explain that.