Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Concept
Standard ML
Summary
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.
Standard ML is a modern dialect of ML, the language used in the Logic for Computable Functions (LCF) theorem-proving project. It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML.
Standard ML is a functional programming language with some impure features. Programs written in Standard ML consist of expressions as opposed to statements or commands, although some expressions of type unit are only evaluated for their side-effects.
Like all functional languages, a key feature of Standard ML is the function, which is used for abstraction. The factorial function can be expressed as follows:
fun factorial n =
if n = 0 then 1 else n * factorial (n - 1)
An SML compiler must infer the static type without user-supplied type annotations. It has to deduce that is only used with integer expressions, and must therefore itself be an integer, and that all terminal expressions are integer expressions.
The same function can be expressed with clausal function definitions where the if-then-else conditional is replaced with templates of the factorial function evaluated for specific values:
fun factorial 0 = 1
| factorial n = n * factorial (n - 1)
or iteratively:
fun factorial n = let val i = ref n and acc = ref 1 in
while !i > 0 do (acc := !acc * !i; i := !i - 1); !acc
end
or as a lambda function:
val rec factorial = fn 0 => 1 | n => n * factorial (n - 1)
Here, the keyword introduces a binding of an identifier to a value, introduces an anonymous function, and allows the definition to be self-referential.
The encapsulation of an invariant-preserving tail-recursive tight loop with one or more accumulator parameters within an invariant-free outer function, as seen here, is a common idiom in Standard ML.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related publications (1)
District scale prediction of subsurface waste heat flows
Due to increasing urbanization and scarcity of land, the need to include the underground in urban planning is growing, especially in cities. The human-made underground structures generate an anthropogenic heat flow which has a significant impact on the ground temperature and leads to the creation of urban underground heat islands (UUHI). In parallel with the urbanization, the consumption of energy increases and the interest in sustainable energy production from thermal energy sources is growing. The UUHI have a high geothermal potential and are therefore of great interest for energy production. A sustainable evaluation of the geothermal potential in cities depends however on many factors and is therefore a complex procedure in which different scenarios must be assessed. This master thesis proposes a machine learning (ML) based approach for the evaluation of the underground waste heat flow of buildings. ML techniques are suitable to very quick and accurate modeling and can therefore be of great interest in the field of complex geothermal potential evaluation. In this project we will focus on the ground temperature change due to heat losses of basements. To this effect, 2D heat maps are created for a given depth and a given simulation time period. In this study, a comprehensive validation of the proposed ML model (random forest algorithm) is presented for different small scale scenarios, using various heat source geometries, locations, numbers and thermal loads. Furthermore, we study the heat maps for diverse depths and simulation time periods. To do so, we assume only a conductive heat flow mode and constant boundary conditions. The proposed methodology involves having access to fully solved numerical simulation to create a data set which is used to train and test the ML algorithm. For this purpose, the finite element software package COMSOL is used. We evaluate and discuss the accuracy of the proposed ML approach on each studied scenario. The results promise a big potential all while requiring only few solved FE models. We obtain a root mean squared error of always less than 5 to 10% depending on the scenario. At the end of this paper a district scale application of the proposed ML technique is presented on the Loop district in Downtown Chicago, US. It will be shown that 25% of the total Loop data from the FE model is sufficient to learn the ML model and to predict the whole district with a root mean squared error of less than 5%.
2020Related concepts (73)
Poplog
Poplog is an open source, reflective, incrementally compiled software development environment for the programming languages POP-11, Common Lisp, Prolog, and Standard ML, originally created in the UK for teaching and research in Artificial Intelligence at the University of Sussex, and later marketed as a commercial package for software development as well as for teaching and research. It was one of the initiatives supported for a while by the UK government-funded Alvey Programme.
Mercury (programming language)
Mercury is a functional logic programming language made for real-world uses. The first version was developed at the University of Melbourne, Computer Science department, by Fergus Henderson, Thomas Conway, and Zoltan Somogyi, under Somogyi's supervision, and released on April 8, 1995. Mercury is a purely declarative logic programming language. It is related to both Prolog and Haskell. It features a strong, static, polymorphic type system, and a strong mode and determinism system.
Rust (programming language)
Rust is a multi-paradigm, general-purpose programming language that emphasizes performance, type safety, and concurrency. It enforces memory safety—ensuring that all references point to valid memory—without requiring the use of a garbage collector or reference counting present in other memory-safe languages. To simultaneously enforce memory safety and prevent data races, its "borrow checker" tracks the object lifetime of all references in a program during compilation.
Related courses (20)
CS-214: Software construction
Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and
fundam
CS-550: Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
PHYS-100: Advanced physics I (mechanics)
La Physique Générale I (avancée) couvre la mécanique du point et du solide indéformable. Apprendre la mécanique, c'est apprendre à mettre sous forme mathématique un phénomène physique, en modélisant l