I'm interested in programming language theory, particularly in functional languages and type systems. I enjoy thinking about purely theoretical problems, but my work is usually built upon a concrete domain. For instance, I explored the ideas of functional reactive programming in the contexts of music and user interfaces, and more recently, I have been exploring ideas of partial evaluation and delayed/staged typechecking in the context of differential privacy.
I have been working on a language for adaptive differential privacy with Benjamin Pierce. Our language, Adaptive Fuzz, incorporates state of the art adaptive privacy filters into a system framework to allow standard differential privacy mechanisms to be usable in a safe and intuitive way.
My graduate work, under the late Paul Hudak, was on functional reactive programming. I designed a system of resource types for safety and clarity, and worked on a system of asynchronous concurrency. Specifically, I spent much time on the computer music language Euterpea and its arrowized graphical package UISF.
Over the summer of 2011, I interned at Microsoft Research in Cambridge, UK with Simon Marlow. I initially worked on adding data and type declarations to GHCi (see the git commit), and then I worked on new features for the Par monad.
You can find my resume here.
I was on the program committee for PADL (the symposium on the Practical Aspects of Declarative Programming) 16 and 17.
Click on citations for abstracts and BibTex entries.
- A Framework for Adaptive Differential Privacy (2017) [PDF] [Code]
Winograd-Cort, D , Haeberlen, A, Roth, A, and Pierce, B. "A Framework for Adaptive Differential Privacy". In Submission.Abstract
Differential privacy is a widely studied theory for analyzing sensitive data with a strong privacy guarantee---any change in an individual's data can have only a small statistical effect on the result---and a growing number of programming languages now support differentially private data analysis. A common shortcoming of these languages is poor support for adaptivity. In practice, a data analyst rarely wants to run just one function over a sensitive database, nor even a predetermined sequence of functions with fixed privacy parameters; rather, she wants to engage in an interaction where, at each step, both the choice of the next function and its privacy parameters are informed by the results of prior functions. Existing languages support this scenario using a simple composition theorem, which often gives rather loose bounds on the actual privacy cost of composite functions, substantially reducing how much computation can be performed within a given privacy budget. The theory of differential privacy includes other theorems with much better bounds, but these have not yet been incorporated into programming languages.
We propose a novel framework for adaptive composition that is elegant, practical, and implementable. It consists of a reformulation based on typed functional programming of the privacy filters of Rogers et al. (2016), together with a concrete realization of this framework in the design and implementation of a new language, called Adaptive Fuzz. Adaptive Fuzz transplants the core static type system of Fuzz to the adaptive setting by wrapping the Fuzz typechecker and runtime system in an outer adaptive layer, allowing Fuzz programs to be conveniently constructed and typechecked on the fly. We describe an interpreter for Adaptive Fuzz and report results from two case studies demonstrating its effectiveness for implementing common statistical algorithms over real data sets.
- Partial Evaluation for Typechecking (In Submission) [PDF]
Winograd-Cort, D, Zhang, H, and Pierce, B. Partial Evaluation for Typechecking. In Submission.Abstract
We study a small functional language in which programs are partially evaluated before typechecking, achieving some of the useful effects of preprocessors, template systems, and macros in a pleasantly straightforward way. We present the system three ways—a declarative formulation reflecting the programmer’s view of its behavior, a nondeterministic algorithm uniformly capturing a wide range of possible heuristic choices about how an implementation might interleave partial evaluation and typechecking, and a concrete instance embodying one specific set of heuristics—and show that all three produce the same typings "in the limit." We also show that the system enjoys standard properties including unicity of types, progress, and preservation.
- A Framework for Adaptive Differential Privacy (2016) [Poster]
Winograd-Cort, D , Haeberlen, A, Roth, A, and Pierce, B. A Framework for Adaptive Differential Privacy. In Theory and Practice of Differential Privacy, New York, New York, June 2016.
- Effects, Asynchrony, and Choice in Arrowized Functional Reactive Programming (2015) [Official PDF, Single-Spaced PDF, Defense Slides]
Winograd-Cort, D. Effects, Asynchrony, and Choice in Arrowized Functional Reactive Programming. PhD thesis, Yale University, December 2015.
- Communicating Functional Reactive Processes (unpublished) [Contact me if you are interested in seeing a draft]
Winograd-Cort, Daniel and Hudak, Paul. Communicating Functional Reactive Processes. Unpublished.Abstract
Functional Reactive Programming (FRP) is a model that facilitates programming real-time and reactive systems by utilizing signal functions that transform streams of inputs into streams of outputs. One of the great benefits of FRP is that it allows the programmer to assume that instantaneous values on those streams are processed infinitely fast, an illusion that we call the Fundamental Abstraction of FRP. To maintain this illusion, FRP enforces a synchronization to the program as a whole. However, when we desire portions of a program to run faster than others, this synchronization becomes a burden.
Introducing asynchrony is not as simple as merely providing an asynchronizing operator---indeed, doing so haphazardly could shatter the fundamental abstraction entirely. However, if we consider each asynchronous process as having its own notion of time and carefully mediate communication between them, we can retain the abstraction on a per-process level and still reap the benefits of asynchrony. We present just such a design, providing demonstrative examples, a formal semantics, and an implementation in Haskell. We call this Communicating Functional Reactive Processes.
- Real-Time Interactive Music in Haskell (2015) [PDF]
Hudak, Paul, Quick, Donya, Santolucito, Mark, and Winograd-Cort, Daniel. "Real-Time Interactive Music in Haskell". In Proceedings of the 3rd ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design, FARM 2015, pages 15–16, New York, NY, USA, 2015. ACM.Abstract
Euterpea and UISF are two recently released Haskell libraries on Hackage that facilitate the creation of interactive musical programs. We show an example of using these two libraries in combination with Haskell’s support for parallelism to create a complex application that generates music in real time in response to user input from MIDI controllers.
- Musical User Interface (2015)
Winograd-Cort, Daniel and Hudak, Paul. Musical User Interface. In Hudak, P, editor, The Haskell School of Music – From Signals to Symphonies. (Version 2.7), January 2015.Information
This is a chapter of the book "The Haskell School of Music – From Signals to Symphonies" that I wrote to provide a Euterpea-centric introduction to the UISF library.
- Settable and Non-Interfering Signal Functions for FRP (2014) [PDF] [Talk (Slides)] [Experimental Code (1) (2)]
Winograd-Cort, Daniel and Hudak, Paul. Settable and Non-Interfering Signal Functions for FRP. In: International Conference on Functional Programming. ACM, September 2014.Abstract
Functional Reactive Programming (FRP) provides a method for programming continuous, reactive systems by utilizing signal functions that, abstractly, transform continuous input signals into continuous output signals. These signals may also be streams of events, and indeed, by allowing signal functions themselves to be the values carried by these events (in essence, signals of signal functions), one can conveniently make discrete changes in program behavior by "switching" into and out of these signal functions. This higher-order notion of switching is common among many FRP systems, in particular those based on arrows, such as Yampa.
Although convenient, the power of switching is often an overkill and can pose problems for certain types of program optimization (such as causal commutative arrows), as it causes the structure of the program to change dynamically at run-time. Without a notion of just-in-time compilation or related idea, which itself is beset with problems, such optimizations are not possible at compile time.
This paper introduces two new ideas that obviate, in a predominance of cases, the need for switching. The first is a non-interference law for arrows with choice that allows an arrowized FRP program to dynamically alter its own structure (within statically limited bounds) as well as abandon unused streams. The other idea is a notion of a settable signal function that allows a signal function to capture its present state and later be restarted from some previous state. With these two features, canonical uses of higher-order switchers can be replaced with a suitable first-order design, thus enabling a broader range of static optimizations.
- Wormholes: Introducing Effects to FRP (2012) [PDF] [Talk]
Winograd-Cort, Daniel and Hudak, Paul. Wormholes: Introducing Effects to FRP. In: Haskell Symposium. ACM, September 2012.Abstract
Functional reactive programming (FRP) is a useful model for programming real-time and reactive systems in which one defines a signal function to process a stream of input values into a stream of output values. However, performing side effects (e.g. memory mutation or input/output) in this model is tricky and typically unsafe. In previous work, Winograd-Cort et al. introduced resource types and wormholes to address this problem.
This paper better motivates, expands upon, and formalizes the notion of a wormhole to fully unlock its potential. We show, for example, that wormholes can be used to define the concept of causality. This in turn allows us to provide behaviors such as looping, a core component of most languages, without building it directly into the language. We also improve upon our previous design by making wormholes less verbose and easier to use.
To formalize the notion of a wormhole, we define an extension to the simply typed lambda calculus, complete with typing rules and operational semantics. In addition, we present a new form of semantic transition that we call a temporal transition to specify how an FRP program behaves over time and to allow us to better reason about causality. As our model is designed for a Haskell implementation, the semantics are lazy. Finally, with the language defined, we prove that our wormholes indeed allow side effects to be performed safely in an FRP framework.
- Virtualizing Real-World Objects in FRP (2012) [PDF] [Haskell Implementors' Workshop Talk]
Winograd-Cort, Daniel and Liu, Hai and Hudak, Paul. Virtualizing Real-World Objects in FRP. In: Practical Aspects of Declarative Languages, volume 7149 of Lecture Notes in Computer Science, pages 227-241. Springer-Verlag, January 2012.Abstract
We begin with a functional reactive programming (FRP) model in which every program is viewed as a signal function that converts a stream of input values into a stream of output values. We observe that objects in the real world – such as a keyboard or sound card – can be thought of as signal functions as well. This leads us to a radically different approach to I/O – instead of treating real-world objects as being external to the program, we expand the sphere of influence of program execution to include them within the program. We call this virtualizing real-world objects. We explore how even virtual objects, such as GUI widgets, and non-local effects, such as are needed for debugging (using something that we call a "wormhole") and random number generation, can be handled in the same way.
Our methodology may at first seem naive – one may ask how we prevent a virtualized device from being copied, thus potentially introducing non-determinism as one part of a program competes for the same resource as another. To solve this problem, we introduce the notion of a resource type that assures that a virtualized object is not duplicated and that I/O and non-local effects are safe. Resource types also provide a deeper level of transparency: by inspecting the type, one can clearly see exactly what resources are being used. We use arrows, type classes, associated types, and type families to implement our ideas in Haskell, and the result is a safe, effective, and transparent approach to stream-based I/O.
- Deducing Relevant Bridge Bidding Information from Double Dummy Data (2008) [PDF]
Winograd-Cort, Daniel. Deducing Relevant Bridge Bidding Information from Double Dummy Data. Brown University undergraduate thesis, May 2008.Abstract
The game of Bridge has entertained card players for many years. The players start by evaluating their hands individually and then using this information to bid for a contract. Bidding systems provide a way for partners to communicate the values of their hands so they can find an appropriate contract, but they are often imprecise and can lead teams into contracts that they cannot keep. Unfortunately, creating a new bidding system is a challenging task. There are approximately 10^28 ways to deal 13 cards each to 4 people from a 52 card deck, but there are 10^47 possible bidding sequences. Therefore, instead of creating a new bidding system, I propose to determine what information is most important to convey in order to achieve success. As opposed to hand evaluation, this system will use relationships between two partners’ hands. For this project, I train neural networks using sample simplified hands of Bridge (known as Double Dummy Bridge results) to find which particular patterns and relationships of cards represent the necessary information needed to complete the best possible contract. Although I am unable to extract meaningful rules from the neural networks to find these combinations, I show the proper steps and the places for improvement.
- From Stirling to Wallis (2005) [Image]
Winograd-Cort, Daniel. From Stirling to Wallis. The Pi Mu Epsilon Journal, Vol. 12-3, Fall 2005.Abstract
A rigorous mathematical proof of Wallis' Formula using infinite series and Stirling's Formula.