Abstract
We discuss a DSL intended for use in an education setting when teaching the writing of interactive Haskell programs to students. The DSL was previously presented as a small formal language of specifications capturing the behavior of simple console I/O programs, along with a trace-based semantics. A prototypical implementation also exists. When going for productive application in an actual course setting, some robustness and usability questions arise. For example, if programs written by students are mechanically checked and graded by the implementation, what guarantees are there for the educator that the assessment is correct? Does the implementation really agree with the on-paper semantics? What else can inform the educator’s writing of a DSL expression when developing a new exercise task? Which activities beyond testing of student submissions can be mechanized based on the specification language? Can we, for example, generate additional material to hand to students in support of task understanding, before, and feedback or trusted sample solutions, after their own solution attempts? Also, how to keep the framework maintainable, preserving its guarantees when the expressiveness of the underlying DSL is to be extended? Our aim here is to address these and related questions, by reporting on connections we have made and concrete steps we have taken, as well as the bigger picture.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In the full formulation from [12], consecutive outputs in generalized traces are additionally normalized into a single output action that chooses from a set of value sequences. We ignore this detail here in favor of a more straightforward presentation.
- 2.
That is easier said than done. We do at the moment not have a general solution to reliably generate “suitable” inputs only, beyond simple typing as expressed by the \(\tau \) in \([\, \triangleright \, x \,]^{\tau }\), and therefore currently rely on using only specifications that do not involve non-terminating behavior for any well-typed inputs at all.
- 3.
There are no guarantees that we can actually use a term constructed with \( getAll \) or \( getCurrent \) at any particular instantiation for type \( a \). Checks happen at runtime.
- 4.
A live online demonstration of the prototype implementation for that previous article is available at https://autotool.fmi.iw.uni-due.de/tfpie19, showcasing the approach. (Note that this demo still uses applicative-style terms.)
- 5.
For notational simplicity, we leave out the continuation and environment here.
- 6.
Of course, one has to take scoping and types into account as well.
- 7.
More precisely, we choose a random and unconditionally reached position.
- 8.
- 9.
A Haskell version can be found at http://hackage.haskell.org/package/quickcheck-state-machine.
References
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: International Conference on Functional Programming, Proceedings, pp. 268–279. ACM (2000). https://doi.org/10.1145/351240.351266
Filinski, A.: Controlling effects. Ph.D. thesis, Carnegie Mellon University (1996)
Gibbons, J., Wu, N.: Folding domain-specific languages: deep and shallow embeddings (Functional Pearl). In: International Conference on Functional Programming, Proceedings, pp. 339–347. ACM (2014). https://doi.org/10.1145/2628136.2628138
Hughes, J.: QuickCheck testing for fun and profit. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 1–32. Springer, Heidelberg (2006). https://doi.org/10.1007/978-3-540-69611-7_1
Hughes, J.: Experiences with QuickCheck: testing the hard stuff and staying sane. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 169–186. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30936-1_9
Liang, S., Hudak, P., Jones, M.P.: Monad transformers and modular interpreters. In: Principles of Programming Languages, Proceedings, pp. 333–343. ACM (1995). https://doi.org/10.1145/199448.199528
McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1–13 (2008). https://doi.org/10.1017/S0956796807006326
Peyton Jones, S.L., Wadler, P.: Imperative functional programming. In: Principles of Programming Languages, Proceedings, pp. 71–84. ACM (1993). https://doi.org/10.1145/158511.158524
Siegburg, M., Voigtländer, J., Westphal, O.: Automatische Bewertung von Haskell-Programmieraufgaben. In: Proceedings of the Fourth Workshop “Automatische Bewertung von Programmieraufgaben”, pp. 19–26. GI (2019). https://doi.org/10.18420/abp2019-3
Swierstra, W., Altenkirch, T.: Beauty in the beast – a functional semantics for the awkward squad. In: Haskell Workshop, Proceedings, pp. 25–36. ACM (2007). https://doi.org/10.1145/1291201.1291206
Waldmann, J.: Automatische Erzeugung und Bewertung von Aufgaben zu Algorithmen und Datenstrukturen. In: Proceedings of the Third Workshop “Automatische Bewertung von Programmieraufgaben”, CEUR Workshop Proceedings, vol. 2015. CEUR-WS.org (2017)
Westphal, O., Voigtländer, J.: Describing console I/O behavior for testing student submissions in Haskell. In: Eighth and Ninth International Workshop on Trends in Functional Programming in Education, Proceedings, EPTCS, vol. 321, pp. 19–36. EPTCS (2020). https://doi.org/10.4204/EPTCS.321.2
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Westphal, O., Voigtländer, J. (2020). Implementing, and Keeping in Check, a DSL Used in E-Learning. In: Nakano, K., Sagonas, K. (eds) Functional and Logic Programming. FLOPS 2020. Lecture Notes in Computer Science(), vol 12073. Springer, Cham. https://doi.org/10.1007/978-3-030-59025-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-59025-3_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-59024-6
Online ISBN: 978-3-030-59025-3
eBook Packages: Computer ScienceComputer Science (R0)