{"id":1791,"date":"2014-09-02T06:54:37","date_gmt":"2014-09-02T06:54:37","guid":{"rendered":"http:\/\/www.syslog.cl.cam.ac.uk\/?p=1791"},"modified":"2016-10-04T13:22:38","modified_gmt":"2016-10-04T13:22:38","slug":"icfp-2014-day-2","status":"publish","type":"post","link":"https:\/\/www.syslog.cl.cam.ac.uk\/2014\/09\/02\/icfp-2014-day-2\/","title":{"rendered":"ICFP 2014: Day 2"},"content":{"rendered":"
This is day 2 of the 19th International Conference on Functional Programming. Leo and I(Heidi) are here bright and early to bring you the highlights from\u00c2\u00a0Gothenburg, Sweden. We are not the only livebloggers here at ICFP, check out Edward Yang<\/a>'s excellent notes.<\/p>\n Intro: Robby's work on behavioural software co<\/a>ntracts is beautiful :)<\/p>\n Instead of an abstract, the keynote has a bibliography of interesting work in the area<\/p>\n Contracts are infectious<\/p>\n Example of racket code, working in a call-by-value language here a point-in function. Demonstration of contract violation including a blame, from applying bools instead of integers. Robby's adds an contract to guard access to point-in and the blame now points to the top-level.<\/p>\n Graph demonstrating how the number contracts in Racket in git has constantly increased. Robby identifiers the outliers e.g. big libraries with lots of contracts have been introduced. Most commits add 1 contract, if they add any.<\/p>\n Everyone is the audience is thinking, why use contracts when you can use types, as identified by Robby.<\/p>\n Contracts Verse Types: The previous example is used with types instead of contracts and negative integers are used to demonstrate how types are insufficient. He introduces a dependant contract, hinting at a comparison to dependent types. We have the arguments at the time of checking unlike dependant types hence its actually possible in real languages.<\/p>\n Switch to an example of a function called dc, which takes a drawing function and bonding box and draws as a side effect. Robby introduces a broken function, which introduces state pollution. We can't check that state after equals the state before, but this would be too late. Here's a contract example, generating a random state and testing for state pollution, this doesn't give us complete corrects but its good enough in this contexts.<\/p>\n Don't think about contracts in terms of projections, but in terms of boundaries (work by Christos)<\/p>\n Addition of contacts to simply typed lambda calculus, in particular how monitors add contracts to boundaries. Example of if we have contract (x =< 3), how values of x > 3 causes the function to abort. If we have another contract to checks f's arguments and return values are x=<3, we allow the function to passed though to with extra monitors on return values.<\/p>\n What happens if we have a bug in the monitor ?<\/p>\n Applications: How can contracts work if you don't give have access to the code the other side of the boundary. We can use the contract exercise function to generate random functions to test monitors. We have an notion of whether one contract is stronger than another.<\/p>\n Gradual typing: How we interfere between typed and untyped languages, see how we do it with Typed Racket. This presentation is actually written in racket, all output is real output.<\/p>\n Takeaways: Contracts are not just crappy types, contracts infect code bases, boundaries are vital.<\/p>\n ICFP knows how to prove specifications. Contract infectiousness is our opportunity to share that knowledge with the world<\/p>\n Q: Randomisation would break formal tools, why not use NaN ? Q: Contracts are checked at runtime, what about the overhead ? Is there a switch to turn it off ? Q: Effects are alarming ! Q: Why can't we introduce randomness to type checking ... ? Q: Thank you for the cross community impact !<\/p>\n Q: How is the blaming system implemented ? Can we add it to python or C ? Q: The opposite of gradual typing, often checks aren't just typed based. Can we use types to check for placement of contracts ? Q: Dependent contracts seems to explicitly pass all arguments, its looks a bit strange ? <\/p>\n <\/p>\n Session 6: Contracts & Scheme (Chair: Michael Sperber)<\/strong><\/p>\n This is the snake game with contracts, most computation time is executing contracts not code, there is serious overhead.<\/p>\n Contract and blame avoidance cycle, how can we then introduce static contract verification.<\/p>\n We will consider soft contract verification: CPCF<\/p>\n Introduce PCF language, and introducing contract notation.<\/p>\n How can we verify CPCF ? We abstract CPCF function to a type, symbolic values are sets of contracts. Check refine values are they flow through, these refines can influence the computation.<\/p>\n Theorem: Verified modules can't be blamed - Proved Contracts fail at first order, only need a F.O solver for verification Q: How to do you handle recursion ? This is course in problem solving, not functional programming<\/p>\n Process: Example of 2D-tree data definition and writing a function to find the nearest point.<\/p>\nKeynote (Chair: Jesse Tov)<\/strong><\/h4>\n
Behavioral Software Contracts
\nSpeaker: Robert Bruce Findler (Northwestern University)<\/em><\/h4>\n
\nStatic Analysis: Havic, exhaustive boundary checking<\/p>\n
\nA: Just setting to default may not find errors<\/p>\n
\nA: There's no kill switch, but there are option contracts<\/p>\n
\nA: Well, it doesn't alarm me, its vital for practical code and we need to look into this further<\/p>\n
\nA: that the point<\/p>\n
\nA: Fundamentally we could do this, we would love to see more of this.<\/p>\n
\nA: Contracts are specification, they can be wrong like normal programs.<\/p>\n
\nA: Explicitly labelling dependency makes it cheaper<\/p>\n
\nSoft Contract Verification
\nPhuc C. Nguyen (University of Maryland); Sam Tobin-Hochstadt (Indiana University); David Van Horn (University of Maryland)<\/em><\/h4>\n
\n- we can analysis first class contracts
\n- using SMT solver
\n- competitive
\n- works even without apparent contracts<\/p>\n
\nSoundness: All concentration are approximated by CPCF<\/p>\n
\nWe proof well to soft typing, occurrence typing, H.O recursion schemes and dependent refinements and video games for the beginning.<\/p>\n
\nQ: If we replace with pos? with >4, where you short cutting the SMT solver ?
\nA: Yes, the name was just a shortcut<\/p>\n
\nA: This is described in the paper<\/p>\nOn Teaching How to Design Programs: Observations from a Newcomer
\nNorman Ramsey (Tufts University)<\/em><\/h4>\n
\n1) Describe data, input, making data examples
\n2) Describing functions, making function examples
\n3) Creating code templates from types, fill in the template
\n4) Test, review and re-factor<\/p>\n