Difference between revisions of "NL-FP dag 2017"

From Clean
Jump to navigationJump to search
 
(19 intermediate revisions by the same user not shown)
Line 6: Line 6:
 
meeting new people. Experts and newcomers to the field are equally welcome.
 
meeting new people. Experts and newcomers to the field are equally welcome.
  
The NL-FP day 2017 takes place on Friday, January 6, 2017 at the
+
The NL-FP day 2017 takes place on '''Friday, January 6, 2017''' at the
 
[http://www.ru.nl/ Radboud University] in Nijmegen.
 
[http://www.ru.nl/ Radboud University] in Nijmegen.
  
Line 37: Line 37:
 
== Registration, Cost, Deadline ==
 
== Registration, Cost, Deadline ==
  
Please register by sending an email to [mailto:m.klinik@cs.ru.nl?subject=NLFP2017%20Registration Markus Klinik] including
+
Please register by sending an email to Markus Klinik including
  
 
* Name
 
* Name
Line 53: Line 53:
  
 
== Program ==
 
== Program ==
 
A preliminary sketch of the day.
 
  
 
* 9:30 - 10:15 Registration
 
* 9:30 - 10:15 Registration
 
* 10:15 - 10:20 Welcome and Opening
 
* 10:15 - 10:20 Welcome and Opening
* 10:20 - 10:45 Talk 1
+
* 10:20 - 10:45 Jeroen Bransen - Music in the Cloud
* 10:45 - 11:10 Talk 2
+
* 10:45 - 11:10 Arjan Oortgiese - A Distributed Server Architecture for Task Oriented Programming
 
* 11:10 - 11:40 Break
 
* 11:10 - 11:40 Break
* 11:40 - 12:05 Talk 3
+
* 11:40 - 12:05 [[:File:2017-FP-Dag-TDD-Sessions.pdf|Jan de Muijnck-Hughes - Type-Driven Design of Communicating Systems using Idris]]
* 12:05 - 12:30 Talk 4
+
* 12:05 - 12:30 Guillaume Allais - agdARGS: declarative hierarchical command line interfaces
 
* 12:30 - 14:00 Lunch
 
* 12:30 - 14:00 Lunch
* 14:00 - 14:25 Talk 5
+
* 14:00 - 14:25 Jan Martin Jansen - A Portable VM-based implementation Platform for non-strict Functional Programming Languages
* 14:25 - 14:50 Talk 6
+
* 14:25 - 14:50 Gert-Jan Bottu - Quantified class constraints in Haskell
* 14:50 - 15:15 Talk 7
+
* 14:50 - 15:15 Hendrik Folmer - SLAM on FPGA using CλaSH
 
* 15:15 - 15:45 Break
 
* 15:15 - 15:45 Break
* 15:45 - 16:10 Talk 8
+
* 15:45 - 16:10 Doaitse Swierstra - Build your own ST Monad with Polymorphic Contexts
* 16:10 - 16:35 Talk 9
+
* 16:10 - 16:35 Johan Hidding - Noodles, a functional concurrent programming model for Python
 
* 16:35 - 16:45 Closing
 
* 16:35 - 16:45 Closing
 
* 18:00 Dinner
 
* 18:00 Dinner
Line 88: Line 86:
  
 
[http://www.cs.ru.nl/staff/Markus.Klinik Markus Klinik]
 
[http://www.cs.ru.nl/staff/Markus.Klinik Markus Klinik]
 
m.klinik@cs.ru.nl
 
  
 
== Talks ==
 
== Talks ==
  
=== Jeroen Bransen - Music in the Cloud ===
+
==== Jeroen Bransen - Music in the Cloud ====
  
 
Using Cloud Haskell for automatic chord extraction
 
Using Cloud Haskell for automatic chord extraction
Line 109: Line 105:
 
particular, are used within Chordify and how they have helped Chordify
 
particular, are used within Chordify and how they have helped Chordify
 
to become a successful music e-learning platform.
 
to become a successful music e-learning platform.
 +
 +
==== Johan Hidding - Noodles, a functional concurrent programming model for Python ====
 +
 +
We present a new model for doing parallel/concurent
 +
programming in Python, targeted at managing complex computational
 +
workflows in distributed environments.
 +
The design of this model is geared towards minimal modification of
 +
existing Python code, and ease of use for domain scientists with
 +
limited computational expertise.
 +
We leverage the implicit parallelism present in a Python user-script by
 +
creating a directed acyclic graph of the function calls in the script.
 +
This graph can be executed using one of the available runners, making
 +
the approach scalable from laptop to cluster computer environments.
 +
 +
==== Jan de Muijnck-Hughes - Type-Driven Design of Communicating Systems using Idris ====
 +
 +
The idea of communicating systems is a cornerstone of modern technology and
 +
allows heterogeneous collections of components to communicate through
 +
well-defined protocols. However, there is a disconnect between the tooling and
 +
languages used to design, implement and reason about communication protocols.
 +
 +
Idris is a general purpose programming language that supports full-dependent
 +
types, providing programmers with the ability to reason more precisely about
 +
programs. Inspired by work on session types and algebraic effect handlers our
 +
research looks to leverage such state-of-the-art programming paradigms in a
 +
dependently typed setting to describe and reason about communication protocols
 +
and their implementation in different communication contexts.
 +
 +
This talk presents our current progress and introduces =Sessions=, a library
 +
for describing, and reasoning about, the interactions of a communicating
 +
system. Demonstrated is use of sessions to describe common communication
 +
patterns, and how the library enforces correctness of the pattern itself
 +
through type-level correct-by-construction guarantees.
 +
 +
Given time future work will also be presented detailing our next steps in
 +
linking these descriptions to implementations such that compile time
 +
correctness guarantees over the actions of an entity in a communicating system
 +
can be given respective to a known specification.
 +
 +
==== Arjan Oortgiese - A Distributed Server Architecture for Task Oriented Programming ====
 +
 +
The iTasks framework is a Clean library for developing multi-user, web-enabled applications.
 +
It offers a special flavor of functional programming, Task-Oriented Programming (TOP),
 +
where the notion of tasks play the central role.
 +
In iTasks one specifies the tasks, that end-users and systems have to do to accomplish a certain goal.
 +
From such a specification a central web-server is generated which coordinates the work described.
 +
To provide a specific end-user client with a user-interface for doing the task, web-pages are dynamically generated for the tasks to be done, that can be inspected by any HTML 5 compatible browser.
 +
In this way, any PC, tablet or phone can be used by the end-user to do his or her work.
 +
 +
The current architecture of iTasks is a client-server architecture that is easy to maintain, but it also has certain disadvantages.
 +
The use of one centralized server can become a bottleneck when it has to serve too many clients.
 +
Furthermore, one cannot work offline on tasks when the connection with this central server is lost:
 +
the server constantly needs to administrate the progress clients make.
 +
A feature of the iTask system is that arbitrary complex browser applications can be defined as client.
 +
For this purpose Clean functions are compiled to JavaScript.
 +
But, certainly compared to native Clean code, browsers execute JavaScript code extremely slow,
 +
while only relatively small browser applications can be generated, due to stack size limitations commonly imposed by the standard browsers.
 +
Finally, due to security restrictions, not all resources offered by a platform can be accessed in a browser,
 +
such as the file system or certain hardware like the Bluetooth connection on a tablet or smart phone.
 +
 +
In this paper, we present a solution to address these drawbacks.
 +
In the new iTask architecture one can have an arbitrary topology of distributed iTask controllers.
 +
An iTask controller can act as a server like in the old iTask architecture, as well as a client of some other controller.
 +
The coordination of tasks can be distributed over these controllers, e.g. to decrease the task load of a serving device or to work off-line on a task on a client device.
 +
A first implementation is made that works for Intel and ARM processors running MacOS, Linux, or Windows.
 +
Android Apps can be generated that include a local server, include a browser facility, and have access any resource available on the platform.
 +
 +
We believe our solution is of general interest for anyone who is interested in generating distributed multi-platform applications from one single source code.
 +
 +
==== Guillaume Allais - agdARGS: declarative hierarchical command line interfaces ====
 +
 +
agdARGS is a library for declarative hierarchical command line interfaces. https://github.com/gallais/agdARGS
 +
 +
==== Gert-Jan Bottu - Quantified class constraints in Haskell ====
 +
 +
When making a type an instance of a class in Haskell, it is often necessary to
 +
impose additional constraints on the type variables involved (e.g. equality on
 +
lists is defined via equality on its elements). Currently, the Haskell type
 +
checker limits us to writing only first-order predicates as class constraints.
 +
 +
In this work we investigate all formal aspects of an extension to Haskell's
 +
type system, namely Quantified Class Constraints (first described by R. Hinze
 +
and S. P. Jones). This extension lifts the limitation, allowing programmers to
 +
write higher-order predicates.
 +
 +
This talk illustrates the problem we wish to address and speculates on ways of
 +
addressing the main formal challenges. These include type checking, type
 +
inference and elaboration into System F. Lastly, we will provide a brief
 +
overview of the work to come in the next couple of months.
 +
 +
==== Doaitse Swierstra - Build your own ST Monad with Polymorphic Contexts ====
 +
 +
Most type systems that support polymorphic functions are based on a version of System-F. We argue that this limits useful programming paradigms  for languages with lazy evaluation. We motivate an extension of System-F alleviating this limitation.
 +
 +
We in particular argue that in such languages the relationship between polymorphic and existential types can be made more systematic by allowing to pass back (part of) an existential result of a function call as an argument to the the function call that produced that value.
 +
 +
After presenting our extension to System-F we show how we can implement the strict-state thread monad \ensuremath{\Conid{ST}} by using a returned existential type in specialising the polymorphic function which returns that type. Currently this monad is  built-in into the runtime system of GHC and as such has become part of the language.
 +
 +
==== Hendrik Folmer - SLAM on FPGA using CλaSH ====
 +
 +
SLAM stands for simultaneous localization and mapping and is a mathematical
 +
problem in robotics with a potentially heavy computational load which is
 +
usually solved on a large computational system. Large computational systems
 +
consume a lot of energy which is not ideal for mobile robots. A field
 +
programmable gate array (FPGA) allow developers to create reconfigurable
 +
hardware architectures which could be more efficient in terms of energy
 +
compared to standard computer systems because it has parallel capabilities.
 +
 +
One aspect of SLAM is ICP (Iterative Closest Point). ICP is used to find
 +
the transformation between two sensor observations (laser range scans) to
 +
determine the movement of the robot. In this talk we explore a way how an
 +
ICP algorithm could be realized on an FPGA using the functional hardware
 +
description language CλaSH.
 +
 +
==== Jan Martin Jansen - A Portable VM-based implementation Platform for non-strict Functional Programming Languages ====
 +
 +
The Web has become a paramount deployment platform for computer
 +
applications. Modern Web-application require execution of code on both
 +
server- and client-side. For the client-side JavaScript is the more-or-less
 +
default platform for execution of code. Users of Functional Programming
 +
languages like Haskell and Clean, who want to develop their software
 +
completely in these languages, should rely on dedicated methods to
 +
transform their code to something that can be executed on top of
 +
JavaScript. In this talk we introduce a Virtual Machine that is capable of
 +
efficient execution of bytecode generated by a compiler for a non-strict
 +
intermediate functional language. The virtual machine has several
 +
implementations supporting the same bytecode, including JavaScript and
 +
asm.js versions. In this way we obtain a portable execution platform for
 +
non-strict Functional languages with a better client-side performance than
 +
existing client-side execution platforms.
  
 
== Past NL-FP Days ==
 
== Past NL-FP Days ==

Latest revision as of 11:21, 9 January 2017

The Dutch Functional Programming Day is an annual gathering of researchers, students, and practitioners sharing a common interest in functional programming. The day features talks that cover the latest advances in research, teaching, and applications in the functional programming area. Coffee and lunch breaks provide ample opportunity for networking with your colleagues and meeting new people. Experts and newcomers to the field are equally welcome.

The NL-FP day 2017 takes place on Friday, January 6, 2017 at the Radboud University in Nijmegen.

Location

The FP dag takes place in room LIN 4, Linnaeusgebouw, Heyendaalseweg 137, 6525 AJ Nijmegen.

OpenStreetMap

Google Maps

uvb-linnaeus.jpg

How to get there

From Station Heyendaal to the Linnaeusgebouw

From Nijmegen Central Station, take any of the following busses to the bus stop Huygensgebouw.

  • 10 Heyendaal Shuttle (every 4 minutes)
  • 11 Beuningen Aalsterveld
  • 12 Druten Busstation
  • 13 Wijchen
  • 14 Brakkenstein
  • 15 Wijchen
  • 300 Nijmegen via Bemmel

The building is directly opposite of the bus stop.

Alternatively, there is a local train from the central station to the station "Nijmegen Heyendaal", from where you have to walk southwards over the bridge until you see the building on your left.

Registration, Cost, Deadline

Please register by sending an email to Markus Klinik including

  • Name
  • Affiliation
  • Whether you want to give a talk
  • Whether you want to participate in the dinner (please indicate dietary restrictions)

If you want to give a talk, please include the title and a short abstract. Aim for 20 minutes plus 5 minutes discussion.

There are no participation costs except for dinner, which everybody pays for themselves.

There is a soft registration deadline at the end of this year, primarily because we need to make dinner reservations.

Participants

Program

  • 9:30 - 10:15 Registration
  • 10:15 - 10:20 Welcome and Opening
  • 10:20 - 10:45 Jeroen Bransen - Music in the Cloud
  • 10:45 - 11:10 Arjan Oortgiese - A Distributed Server Architecture for Task Oriented Programming
  • 11:10 - 11:40 Break
  • 11:40 - 12:05 Jan de Muijnck-Hughes - Type-Driven Design of Communicating Systems using Idris
  • 12:05 - 12:30 Guillaume Allais - agdARGS: declarative hierarchical command line interfaces
  • 12:30 - 14:00 Lunch
  • 14:00 - 14:25 Jan Martin Jansen - A Portable VM-based implementation Platform for non-strict Functional Programming Languages
  • 14:25 - 14:50 Gert-Jan Bottu - Quantified class constraints in Haskell
  • 14:50 - 15:15 Hendrik Folmer - SLAM on FPGA using CλaSH
  • 15:15 - 15:45 Break
  • 15:45 - 16:10 Doaitse Swierstra - Build your own ST Monad with Polymorphic Contexts
  • 16:10 - 16:35 Johan Hidding - Noodles, a functional concurrent programming model for Python
  • 16:35 - 16:45 Closing
  • 18:00 Dinner

Dinner

After the program at the university we will have dinner at the restaurant De Hemel. They are going to serve us their Diner Churrasco. We'll be sitting in the Brouwerszaal where they actually brew the beer they serve. For people wo eat neither meat nor fish there are vegetarian options, but we have to tell them beforehand. The menu costs about 30 EUR, drinks not included. Everybody pays for themselves.

We'll go there by public transport. To find the way, team up with one of the locals or use modern technology.

De Hemel
Restaurant & Brouwerscafe
Franseplaats 1
6511 VS Nijmegen
OpenStreetMap

Contact

Markus Klinik

Talks

Jeroen Bransen - Music in the Cloud

Using Cloud Haskell for automatic chord extraction

Chordify is a music e-learning platform that transforms any music source, such as a YouTube video, into chords. Learning to play your favorite songs has never been easier, it's like karaoke for the fingers. Chordify attracts 1.5M visitors every month, we have 550k registered users, and chordified over 4.8M songs.

The automatic chord extraction algorithm is implemented in Haskell. The work is distributed over multiple servers using the Cloud Haskell framework, which makes our service scalable and reliable. In this talk we show how functional programming, and the Cloud Haskell framework in particular, are used within Chordify and how they have helped Chordify to become a successful music e-learning platform.

Johan Hidding - Noodles, a functional concurrent programming model for Python

We present a new model for doing parallel/concurent programming in Python, targeted at managing complex computational workflows in distributed environments. The design of this model is geared towards minimal modification of existing Python code, and ease of use for domain scientists with limited computational expertise. We leverage the implicit parallelism present in a Python user-script by creating a directed acyclic graph of the function calls in the script. This graph can be executed using one of the available runners, making the approach scalable from laptop to cluster computer environments.

Jan de Muijnck-Hughes - Type-Driven Design of Communicating Systems using Idris

The idea of communicating systems is a cornerstone of modern technology and allows heterogeneous collections of components to communicate through well-defined protocols. However, there is a disconnect between the tooling and languages used to design, implement and reason about communication protocols.

Idris is a general purpose programming language that supports full-dependent types, providing programmers with the ability to reason more precisely about programs. Inspired by work on session types and algebraic effect handlers our research looks to leverage such state-of-the-art programming paradigms in a dependently typed setting to describe and reason about communication protocols and their implementation in different communication contexts.

This talk presents our current progress and introduces =Sessions=, a library for describing, and reasoning about, the interactions of a communicating system. Demonstrated is use of sessions to describe common communication patterns, and how the library enforces correctness of the pattern itself through type-level correct-by-construction guarantees.

Given time future work will also be presented detailing our next steps in linking these descriptions to implementations such that compile time correctness guarantees over the actions of an entity in a communicating system can be given respective to a known specification.

Arjan Oortgiese - A Distributed Server Architecture for Task Oriented Programming

The iTasks framework is a Clean library for developing multi-user, web-enabled applications. It offers a special flavor of functional programming, Task-Oriented Programming (TOP), where the notion of tasks play the central role. In iTasks one specifies the tasks, that end-users and systems have to do to accomplish a certain goal. From such a specification a central web-server is generated which coordinates the work described. To provide a specific end-user client with a user-interface for doing the task, web-pages are dynamically generated for the tasks to be done, that can be inspected by any HTML 5 compatible browser. In this way, any PC, tablet or phone can be used by the end-user to do his or her work.

The current architecture of iTasks is a client-server architecture that is easy to maintain, but it also has certain disadvantages. The use of one centralized server can become a bottleneck when it has to serve too many clients. Furthermore, one cannot work offline on tasks when the connection with this central server is lost: the server constantly needs to administrate the progress clients make. A feature of the iTask system is that arbitrary complex browser applications can be defined as client. For this purpose Clean functions are compiled to JavaScript. But, certainly compared to native Clean code, browsers execute JavaScript code extremely slow, while only relatively small browser applications can be generated, due to stack size limitations commonly imposed by the standard browsers. Finally, due to security restrictions, not all resources offered by a platform can be accessed in a browser, such as the file system or certain hardware like the Bluetooth connection on a tablet or smart phone.

In this paper, we present a solution to address these drawbacks. In the new iTask architecture one can have an arbitrary topology of distributed iTask controllers. An iTask controller can act as a server like in the old iTask architecture, as well as a client of some other controller. The coordination of tasks can be distributed over these controllers, e.g. to decrease the task load of a serving device or to work off-line on a task on a client device. A first implementation is made that works for Intel and ARM processors running MacOS, Linux, or Windows. Android Apps can be generated that include a local server, include a browser facility, and have access any resource available on the platform.

We believe our solution is of general interest for anyone who is interested in generating distributed multi-platform applications from one single source code.

Guillaume Allais - agdARGS: declarative hierarchical command line interfaces

agdARGS is a library for declarative hierarchical command line interfaces. https://github.com/gallais/agdARGS

Gert-Jan Bottu - Quantified class constraints in Haskell

When making a type an instance of a class in Haskell, it is often necessary to impose additional constraints on the type variables involved (e.g. equality on lists is defined via equality on its elements). Currently, the Haskell type checker limits us to writing only first-order predicates as class constraints.

In this work we investigate all formal aspects of an extension to Haskell's type system, namely Quantified Class Constraints (first described by R. Hinze and S. P. Jones). This extension lifts the limitation, allowing programmers to write higher-order predicates.

This talk illustrates the problem we wish to address and speculates on ways of addressing the main formal challenges. These include type checking, type inference and elaboration into System F. Lastly, we will provide a brief overview of the work to come in the next couple of months.

Doaitse Swierstra - Build your own ST Monad with Polymorphic Contexts

Most type systems that support polymorphic functions are based on a version of System-F. We argue that this limits useful programming paradigms for languages with lazy evaluation. We motivate an extension of System-F alleviating this limitation.

We in particular argue that in such languages the relationship between polymorphic and existential types can be made more systematic by allowing to pass back (part of) an existential result of a function call as an argument to the the function call that produced that value.

After presenting our extension to System-F we show how we can implement the strict-state thread monad \ensuremath{\Conid{ST}} by using a returned existential type in specialising the polymorphic function which returns that type. Currently this monad is built-in into the runtime system of GHC and as such has become part of the language.

Hendrik Folmer - SLAM on FPGA using CλaSH

SLAM stands for simultaneous localization and mapping and is a mathematical problem in robotics with a potentially heavy computational load which is usually solved on a large computational system. Large computational systems consume a lot of energy which is not ideal for mobile robots. A field programmable gate array (FPGA) allow developers to create reconfigurable hardware architectures which could be more efficient in terms of energy compared to standard computer systems because it has parallel capabilities.

One aspect of SLAM is ICP (Iterative Closest Point). ICP is used to find the transformation between two sensor observations (laser range scans) to determine the movement of the robot. In this talk we explore a way how an ICP algorithm could be realized on an FPGA using the functional hardware description language CλaSH.

Jan Martin Jansen - A Portable VM-based implementation Platform for non-strict Functional Programming Languages

The Web has become a paramount deployment platform for computer applications. Modern Web-application require execution of code on both server- and client-side. For the client-side JavaScript is the more-or-less default platform for execution of code. Users of Functional Programming languages like Haskell and Clean, who want to develop their software completely in these languages, should rely on dedicated methods to transform their code to something that can be executed on top of JavaScript. In this talk we introduce a Virtual Machine that is capable of efficient execution of bytecode generated by a compiler for a non-strict intermediate functional language. The virtual machine has several implementations supporting the same bytecode, including JavaScript and asm.js versions. In this way we obtain a portable execution platform for non-strict Functional languages with a better client-side performance than existing client-side execution platforms.

Past NL-FP Days