-
I’m going as well. Everyone is also encouraged to attend the collocated, free PrlConf event, where we’ll have some really cool talks on the structural and behavioral foundations of programming languages!
-
-
@asthasr Sorry I didn’t see your question until now… PrlConf is an intermediate-to-advanced workshop; we will have some introductory talks interspersed with more advanced ones, but since it’s a small and informal thing, beginners should feel free to come and avail themselves of the speakers' expertise. We have an “all questions are good questions” policy! It is an all-day event.
-
-
-
I read the “Simple Easy!” paper long ago, but this presentation is quite a bit easier to digest w.r.t. the plain nuts and bolts of your bidirectional type checker. Thanks for writing it up, Danny!
-
Yeah, I didn’t mean to but I guess I ended up with a nice presentation of Simple Easy!
I’m still entirely dissatisfied with how bindings are handled :/ Since it’s like all the warts of DeBruijn with some of the quirks of explicit names with just a dash of odd HOAS tossed in. Variables are hard, we should just use SKI.
-
-
-
Fwiw, it is non-trivial in Bound to do type-checking with contexts and working under binders. Larry Diehl has learnt some techniques for doing so in the course of using it in Spire, but it is extremely difficult.
-
-
-
-
-
-
Nice job, thanks for posting this!
Inspired by you, I tried my hand at a different presentation of a bidirectional type checker for a dependently typed lambda calculus. My emphasis was different:
I focussed on providing a presentation that directly represented the judgements of the theory in the program, complete with a notion of analytic and synthetic judgement.
I experimented with really nice error tracing for type errors (judgement refutations).
I used Unbound to avoid having to deal with fiddly integer parameters and substitutions. I like the convenience of Unbound, but it comes at a price: severe anti-modularity.
I also have a cumulative, predicative hierarchy of universes, as well as an intensional identity type.
I do not have inferable and checkable terms in separate syntactic categories, nor do I have a type of “values”. It would be interesting to improve my representation in this way, and then implement NBE.
The main bit of my type checker is here: https://github.com/jonsterling/itt-bidirectional/blob/master/src/TT/Judgement/Bidirectional.hs, but do browse the other files.
-
I spoke about Vinyl 0.4, and its denotation in Type Theory, at BayHac this weekend.
Slides (PDF link): https://github.com/VinylRecords/BayHac2014-Talk/blob/master/Talk.pdf Recording of slides w/ voice: https://vimeo.com/95694918
-
This is really fascinating work, Jon. This has introduced me to a number of new features I didn’t know existed.
Are you concerned that such “duck typing” on records w.r.t. their field names might lead to loss of the very safety Haskell works so hard to guarantee? One can imagine two record types which from separate frameworks, one of which has the fields “name” and “size,” (maybe a key for a cache table of encoded data) and the other of which has those names plus “color” (referring to, say, a shape entity in a drawing application). The former is technically a subtype of the latter, as you’ve defined subtyping, but those fields are semantically distinct, and the type intersection is actually pretty meaningless.
-
Thanks, Andy, that’s a really good question. This seems to be one of the primary weaknesses of structural typing… One thing that could be done to get around it would be to generalize
Fieldto be polymorphic over the kind of its key; that way, when desiring guarantees that your spurious relations to not arise between your records and those of other modules, you could use your own universe of keys, like so:data (:::) :: k -> * -> * where Field :: s ::: t data LocallyAvailableFields = Name | Age name = Field :: Name ::: String age = Field :: Age ::: Int man = (name, "jon") :& (age, 20) :& RNilAnother thing that might be done would be to abstract out even the field representation itself; this would make the implementation a bit more complicated, but it would allow easy declaration of local “field universes”:
data MyFields :: * -> * where Name :: MyFields String Age :: MyFields Int man = (Name, "jon") :& (Age, 20) :& RNilI sort of like this approach, but I haven’t yet thought through its implications on the rest of the system; currently a lot depends on the structure of the field representation, but it may be possible to abstract that away and allow something like what I have proposed above.
-
And it looks like we have our first act of withdrawl over this decision
I wasn’t going to attend in any event, but it does seem rather a waste to throw away a known good on the basis of a remote evil. It’s great publicity for a biased summary of a decision, sure, but doesn’t this negatively impact the folks that could’ve learned something there?
[Comment removed by author]
Hey. I’m really sorry that we cancelled PrlConf and that you were looking forward to it—We are devastated; all of us worked so hard to put together an event that would be fun, educational and inspiring, both for our speakers and for our attendees. However, we had no other option: I could not in good conscience participate in LambdaConf anymore, and most of the PrlConf speakers were no longer going to attend—even if we had not cancelled the event, the event would not have happened in the same sense as it would have under different circumstances. I am so sad that it turned out this way, and I will try to do a better job next year in finding a venue that fits with our values. Please feel free to email me if you have any questions (jon[at]jonmsterling[dot]com), and I am happy to discuss it with you. Again, please accept our apologies for this awful turn of events.
And if you have made nonrefundable travel arrangements in order to attend PrlConf, also please contact me and I will try to help.
You do realize that you’ve done more tangible harm to the people who would’ve gone to your event than might’ve been suffered otherwise, right?
Could you explain your reasoning here in-depth a little?
Would you prefer that we had put on PrlConf without any speakers? I am not sure what you’re asking me to have done…
Let me say, as one of the people who think Lambda made the right decision, that I also think the decision to withdraw may have been the right call for you. You kinda threw the LC folks under the bus with your message imo, but I would never expect people to attend a conference they didn’t want to.
John De Goes is actually my employer, and we had discussed this at length prior to our announcement. John is also someone I consider a good and respected friend.
Ah, so if I understand your position, it was that the speakers you were relying on were going to boycott anyways?
That does force your hand somewhat, I suppose.
EDIT: Am with tedu on this. I disagree with your professed reason, but you can hardly be expected to round up your speakers at gunpoint and for them to present!
That’s a strawman on a slippery slope.