Hume (programming language)

Hume
Paradigm	Functional
Family	Haskell
Designed by	Kevin Hammond Greg Michaelson[ citation needed ]
Developers	University of St Andrews Heriot-Watt University
First appeared	2000;26 years ago (2000)
Stable release	0.8 / 25 April 2008;17 years ago (2008-04-25)
Typing discipline	Inferred, static, strong
Platform	IA-32, PowerPC
OS	macOS, Red Hat Linux
Influenced by
Haskell

Hume Statue in Edinburgh

Hume is a functionally based programming language developed at the University of St Andrews and Heriot-Watt University in Scotland since the year 2000. The language name is both an acronym meaning 'Higher-order Unified Meta-Environment' and an honorific to the 18th-century philosopher David Hume. It targets real-time computing embedded systems, aiming to produce a design that is both highly abstract, and yet allows precise extraction of time and space execution costs. This allows guaranteeing the bounded time and space demands of executing programs.

Hume combines functional programming ideas with ideas from finite-state automata. Automata are used to structure communicating programs into a series of "boxes", where each box maps inputs to outputs in a purely functional way using high-level pattern-matching. It is structured as a series of levels, each of which exposes different machine properties.

Design model

The Hume language design attempts to maintain the essential properties and features required by the embedded systems domain (especially for transparent time and space costing) whilst incorporating as high a level of program abstraction as possible. It aims to target applications ranging from simple microcontrollers to complex real-time systems such as smartphones. This ambitious goal requires incorporating both low-level notions such as interrupt handling, and high-level ones of data structure abstraction etc. Such systems are programmed in widely differing ways, but the language design should accommodate such varying requirements.

Hume is a three-layer language: an outer (static) declaration/metaprogramming layer, an intermediate coordination layer describing a static layout of dynamic processes and the associated devices, and an inner layer describing each process as a (dynamic) mapping from patterns to expressions. The inner layer is stateless and purely functional.

Rather than attempting to apply cost modeling and correctness proving technology to an existing language framework either directly or by altering a more general language (as with e.g., RTSJ), the approach taken by the Hume designers is to design Hume in such a way that formal models and proofs can definitely be constructed. Hume is structured as a series of overlapping language levels, where each level adds expressibility to the expression semantics, but either loses some desirable property or increases the technical difficulty of providing formal correctness/cost models. ^[1]

Characteristics

The interpreter and compiler versions differ a bit.

• the interpreter (concept prover) admits timeout and custom exceptions.
• the compiler admits heap and stack cost bounding but exceptions only print the exception name.

The coordination system wires boxes in a dataflow programming style.

The expression language is Haskell-like.

The message passing concurrency system remembers JoCaml's join-patterns or Polyphonic C Sharp chords, but with all channels asynchronous.

There is a scheduler built-in that continuously checks pattern-matching through all boxes in turn, putting on hold the boxes that cannot copy outputs to busy input destinations.

Examples

Vending machine

dataCoins=Nickel|Dime|Fake;dataDrinks=Coffee|Tea;dataButtons=BCoffee|BTea|BCancel;typeInt=int32;exceptionEFakeCoin::(Int,string);showv=vasstring;boxcoffeein(coin::Coins,button::Buttons,value::Int)-- input channelsout(drink_outp::string,value’::Int,refund_outp::string,display::string)-- named outputswithin500KB(400B)-- max heap ( max stack) cost boundinghandlesEFakeCoin,TimeOut,HeapOverflow,StackOverflowmatch-- * wildcards for unfilled outputs, and unconsumed inputs(my_coin,*,v){- ''join-pattern'' equivalent: coin(my_coin) & value(v) -}->letv’=incrementCreditmy_coinvin(*,v’,*,showv’)-- time bounding (''within x time-unit'') raises TimeOut ()|(*,BCoffee,v){- ''join-pattern'' equivalent: button(BCoffee) & value(v) -}->(vendCoffee10v)within30s|(*,BTea,v)->(vendTea5v)within30s|(*,BCancel,v)->letrefundu="Refund "++showu++"\n"in(*,0,refundv,*)handleEFakeCoin(v,msg)->(*,v,*,msg)|TimeOut()->(*,*,*,"maybe content exhausted, call service!")|HeapOverflow()->(*,*,*,"error: heap limit exceeded")|StackOverflow()->(*,*,*,"error: stack limit exceeded");incrementCreditcoinv=casecoinofNickel->v+5Dime->v+10Fake->raiseEFakeCoin(v,"coin rejected");venddrinkcostv=ifv>=costthen(servedrink,v-cost,*,"your drink")else(*,v,*,"money is short of "++show(cost-v));servedrink=casedrinkofCoffee->"Coffee\n"Tea->"Tea\n";boxcontrolin(c::char)out(coin::Coins,button::Buttons)match'n'->(Nickel,*)|'d'->(Dime,*)|'f'->(Fake,*)|'c'->(*,BCoffee)|'t'->(*,BTea)|'x'->(*,BCancel)|_->(*,*);streamconsole_outpto"std_out";streamconsole_inpfrom"std_in";-- dataflowwirecoffee-- inputs (channel origins)(control.coin,control.button,coffee.value’initially0)-- -- outputs destinations(console_outp,coffee.value,console_outp,console_outp);wirecontrol(console_inp)(coffee.coin,coffee.button);

References

1. Eekelen, Marko Van (2007). Trends in Functional Programming. Intellect Books. p. 198. ISBN   978-1-84150-176-5.

Further reading

• Patai, Gergely; Hanak, Peter (2007). "Embedded Functional Programming in Hume" (PDF). Archived from the original (PDF) on 23 December 2016.

External links

• The Hume Programming Language web site
• The Hume Project at Heriot-Watt University
• EmBounded project, certifies resource-bounded code in Hume
• Hume and Multicore