Home

The Habit Programming Language: The Revised Preliminary Report

Habit is a systems programming dialect of Haskell from the High-Assurance Systems Programming (HASP) project at Portland State University. From The Habit Programming Language: The Revised Preliminary Report

This report presents a preliminary design for the programming language Habit, a dialect of Haskell that supports the development of high quality systems software. The primary commitments of the design are as follows:

* Systems programming: Unlike Haskell, which was intended to serve as a general purpose functional programming language, the design of Habit focusses on features that are needed in systems software development. These priorities are reflected fairly directly in the new features that Habit provides for describing bit-level and memory-based data representations, the introduction of new syntactic extensions to facilitate monadic programming, and, most significantly, the adoption of a call-by-value semantics to improve predictability of execution. The emphasis on systems programming also impacts the design in less direct ways, including assumptions about the expected use of whole program compilation and optimization strategies in a practical Habit implementation.

* High assurance: Although most details of Haskell’s semantics have been formalized at some point in the research literature, there is no consolidated formal description of the whole language. There are also known differences in semantics, particularly with respect to operational behavior, between different Haskell implementations in areas where the Haskell report provides no guidance. Although it is not addressed in the current report, a high-priority for Habit is to provide a full, formal semantics for the complete language that can be used as a foundation for reasoning and formal verification, a mechanism for ensuring consistency between implementations, and a basis for reliably predicting details about memory allocation, asymptotic behavior, and resource utilization.

HASP has a couple of postdoc positions open to help with Habit.

By James Iry at 2011-02-18 16:06 | Functional | Software Engineering | Theory | other blogs | 16212 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Value semantics and Haskell heredity

I made a quick pass at the prelim report, but my lack of a deep understanding of Haskell left me with some questions.

Syntactically this is a Haskell derivative, but how close can it truly be with strict/value evaluation semantics? With Galois involved of course it's announced as a Haskell, but in implementation and semantics will it not need to draw just as strongly from the ML roots?

By Chad Wellington at Fri, 2011-02-18 20:21 | login or register to post comments

There's a history of work on

There's a history of work on strict Haskell variants, including O'Haskell and Timber and now DDC. Arguably, along with syntax, the key things that keep Habit in the Haskell lineage are A) typeclasses, B) purity, and C) monadic handling of effects. In any case, you may want to look more closely at the section on Pointed and Unpointed types, which addresses some of the issues of preserving Haskell semantics in a call-by-value system.

By S. Clover at Fri, 2011-02-18 20:54 | login or register to post comments

Mark Jones, the primary

Mark Jones, the primary designer of Habit, has a long history of contributing to the Haskell community.

Making the semantics call-by-value rather than call-by-need by default doesn't change a Haskell-like type system appreciably, so Habit's new features in the type class design space aren't particularly predicated on either call-by-value or call-by-need semantics. In addition, Habit's approach to effectful programming shares much more with Haskell (that is, there are monads) than with ML.

The members of our team who are working on Habit's semantics are emphasizing denotational semantics, which in some ways is simpler in a call-by-value context.

And of course, there are many possible implementations of Habit, or of any other given language, imaginable, depending on what set of language techniques a particular set of implementors are interested in taking out for a spin!

By Tim Chevalier at Fri, 2011-02-18 22:25 | login or register to post comments

Just to elaborate slightly

Just to elaborate slightly on what Tim said, in addition to features like the type class wonkery and
type-level naturals, many of Habit's features for representing and safely using memory areas would
be equally applicable in Haskell (and were originally presented in a Haskell setting), and the Habit
approach to safe bit-level access is currently being implemented (modulo primitive renaming) as a
GHC language extension.

Choosing a call-by-value semantics (as Tim said) simplifies some of the semantics, as well as
simplifying the runtime machinery (thus reducing verification load) and hopefully making it easier
to reason about the time and memory performance of idiomatic Habit code. There are, of course,
plenty of advantages to a call-by-need semantics, but we have a relatively small research group and
so we have to prioritize. :)

By Garrett Morris at Fri, 2011-02-18 23:34 | login or register to post comments

Thanks all around, the

Thanks all around, the responses were clear even to my eyes. I'll see if I can make a deeper dive in to the un/pointed types section, too.

By Chad Wellington at Sat, 2011-02-19 00:24 | login or register to post comments

diff Haskell Habit

Is there a (however comprehensive) list of design differences between Haskell and Habit?

By Matt M at Fri, 2011-02-18 23:03 | login or register to post comments

The Habit report is written

The Habit report is written for someone who's relatively familiar with Haskell. While it may briefly describe some features that are equivalent in Haskell and Habit, the majority of the text of the report is devoted to the differences. Alternatively, you could look at some of the group's recent language design publications [1,2,3,4]; while this won't give you a complete picture of what we're doing in Habit, and we've changed some design decisions since those publications, it should at least involve fewer pages and more abstracts.

[1] High-level Views on Low-level Representations. Iavor S. Diatchki, Mark P. Jones, and Rebekah Leslie. In Proceedings of the International Conference on Functional Programming (ICFP 2005), Tallinn, Estonia, September 2005.

[2] Strongly Typed Memory Areas. Iavor S. Diatchki, and Mark P. Jones. In Proceedings of the ACM SIGPLAN 2006 Haskell Workshop, Portland, Oregon, September 2006.

[3] Writing Systems Software in a Functional Language: An Experience Report. Iavor S. Diatchki, Thomas Hallgren, Mark P. Jones, Rebekah Leslie, and Andrew Tolmach. In Proceedings of the Fourth Workshop on Programming Languages and Operating Systems (PLOS 2007), sponsored by ACM SIGOPS, Stevenson, Washington, October 2007.

[4] Instance Chains: Type Class Programming Without Overlapping Instances. J. Garrett Morris and Mark P. Jones. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP '10), Baltimore, Maryland, September 27-29, 2010.

By Garrett Morris at Fri, 2011-02-18 23:43 | login or register to post comments

The goal

Since I see a lot of the Habit people are here....

Do you all have a particular aspect of system software you are going after? Do you have something in mind. For example a way to write device drivers that don't pose the same security risks as the ones we have now. Or higher speed video processing that can't memory leak or...?

By JeffB at Sun, 2011-02-20 15:08 | login or register to post comments

I can't speak for the group

I can't speak for the group as a whole, but I don't think there is a specific goal like those you've mentioned. Our proposed demo projects (which the post-doc positions are expected to help with) are an implementation of at least part of an L4 micro-kernel, halVM guests, and an small embedded project. The expected use-cases are pretty broad I think (I'm new to the group so my understanding is limited) -- anything where one would like the sorts of assurances one would expect from a language like haskell, with direct access to memory layout and bit-twiddling built-in to the language. That's all very hand-wavy, I know...

By Andrew Sackville-West at Mon, 2011-02-21 00:01 | login or register to post comments

I don't think there's

I don't think there's necessarily a single goal across all the group. However, we're definitely currently focused on more systems-level tasks; so, while we've got some specific data structures that we need in the L4 implementation, we're not currently trying to write the world's fastest containers library or anything.

Down the road, I'd personally love to see more applications: game engines would be my personal preference, but the applications you've listed are also interesting. The main problem with any of these ideas is funding.

By Garrett Morris at Mon, 2011-02-21 01:11 | login or register to post comments