News aggregator

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega

Lambda the Ultimate - Tue, 11/10/2015 - 8:23am

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega, by Matt Brown and Jens Palsberg:

According to conventional wisdom, a self-interpreter for a strongly normalizing λ-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the normalization barrier and define a self-interpreter for System Fω, a strongly normalizing λ-calculus. After a careful analysis of the classical theorem, we show that static type checking in Fω can exclude the proof’s diagonalization gadget, leaving open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in Fω, including a continuation-passing style transformation. Our operations rely on a new approach to program representation that may be useful in theorem provers and compilers.

I haven't gone through the whole paper, but their claims are compelling. They have created self-interpreters in System F, System Fω and System Fω+, which are all strongly normalizing typed languages. Previously, the only instance of this for a typed language was Girard's System U, which is not storngly normalizing. The key lynchpin appears in this paragraph on page 2:

Our result breaks through the normalization barrier. The conventional wisdom underlying the normalization barrier makes an implicit assumption that all representations will behave like their counterpart in the computability theorem, and therefore the theorem must apply to them as well. This assumption excludes other notions of representation, about which the theorem says nothing. Thus, our result does not contradict the theorem, but shows that the theorem is less far-reaching than previously thought.

Pretty cool if this isn't too complicated in any given language. Could let one move some previously non-typesafe runtime features, into type safe libraries.

Categories: Offsite Discussion

[ANN] SBV 5.4 is out

haskell-cafe - Tue, 11/10/2015 - 5:03am
I'm happy to announce a new release (v5.4) of SBV: SMT Based Verification. See: New in this release is the 'sAssert' function, which allows boolean-assertions to be sprinkled in symbolic code, which can then be statically discharged (or shown violating assignments for) using the 'safe' function. See: A slightly larger example checks for lack-of-division-by-0 in a simple program: Further documentation on SBV is available at: Calls to sAssert calls are also preserved in the SBV->C compilation path. This feature is rather experimental and , and I'd love to hear if you give it a try and see any gotchas.. Happy proving. -Levent. PS. Thanks to Brett Letner for suggesting this functionality. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion

What is the unifying principle of Haskell?

Haskell on Reddit - Mon, 11/09/2015 - 10:31pm

I'm coming from an OO background and trying to learn Haskell not only for its own sake but to better understand the functional paradigm. I learned Smalltalk because it is the purest OO language there is, and so by learning it, you learn OO. Being functionally pure, I expect the same to be true of Haskell.

So my question is: what is the unifying principle of Haskell?

The unifying principle of Smalltalk is object-orientation. Everything is an object, these objects have state, and they are nouns, not verbs.

What would be the equivalent for Haskell? The abstraction which, upon understanding, one has the fundamental building block for designing software with that language.

The closest answer I've found is referential transparency, but it just doesn't seem as powerful an abstraction as the object model. That being said, I just started learning Haskell a few days ago, and have only gone through your basic FP learning exercises, so maybe the enlightenment will come when I start building complex systems with it. That being said, I'd rather be enlightened sooner than later. :)

submitted by dream-spark
[link] [80 comments]
Categories: Incoming News

big number, Haskell

Haskell on Reddit - Mon, 11/09/2015 - 9:07pm
BigNumbers :: Ord a => [a] -> [a] BigNumbers [] = [] BigNumbers (p:xs) = (BigNumbers lesser) ++ [p] ++ (BigNumbers greater) --where -- lesser = filter (< p) xs --greater = filter (>= p) xs

It gave me errors.

200 [ 4,5,800] true 200 [4,5,8] false

how can i got this result

submitted by Germany22221
[link] [10 comments]
Categories: Incoming News

[ANN] New release of SBV (v5.4)

Haskell on Reddit - Mon, 11/09/2015 - 9:05pm
Categories: Incoming News

Reader a-ha moment

Haskell on Reddit - Mon, 11/09/2015 - 7:19pm

For a while, I was a little bit confused about the reader(T) monad. Why bother with the reader monad if the functions you are going to invoke (e.g. from within your do block) don't get access to the reader?

data ConfigFile = ConfigFile { screenWidth :: Int, farewellText :: [String] } main = runReaderT farewell $ ConfigFile 100 ["Goodbye", "human"] farewell = do maxLineLength <- asks screenWidth message <- asks farewellText let formatted = formatMessage message maxLineLength liftIO $ forM_ formatted putStrLn formatMessage message width = filter ((< width) . length) message

The reader is supposed to clean up my argument-passing, but I still have to shovel a bunch of garbage down into the function call. :-(

What to do?

Make it more monadic!

data ConfigFile = ConfigFile { screenWidth :: Int, farewellText :: [String] } main = runReaderT farewell $ ConfigFile 100 ["Goodbye", "human"] farewell = do formatted <- formatMessage liftIO $ forM_ formatted putStrLn formatMessage = do maxLineLength <- asks screenWidth message <- asks farewellText return $ filter ((< maxLineLength) . length) message

This is a pretty basic observation, but it never really was obvious to me. You can arbitrarily nest these monadic invocations, so that the reader-stuff can work its way down into the leaves of your porgram. Hope this helps someone in the future.

submitted by skatenerd
[link] [18 comments]
Categories: Incoming News

why the minimal implementation of Ord is <= instead of <

Haskell on Reddit - Mon, 11/09/2015 - 6:31pm

Given that Ord is also Eq, isn't = given already?

submitted by mr_delphi
[link] [8 comments]
Categories: Incoming News

darcs 2.10.2 release

haskell-cafe - Mon, 11/09/2015 - 4:17pm
The darcs team is pleased to announce the release of darcs 2.10.2 ! # Downloading # The easiest way to install darcs 2.10.2 from source is by first installing the Haskell Platform ( If you have installed the Haskell Platform or cabal-install, you can install this release by doing: $ cabal update $ cabal install darcs-2.10.2 Alternatively, you can download the tarball from and build it by hand as explained in the README file. The 2.10 branch is also available as a darcs repository from # What's new in 2.10.2 (since 2.10.1) # * optimize patch apply code memory use * make patch selection lazier in presence of matchers * switch patches retrieval order when using packs * switch from dataenc (deprecated) to sandi * finish updating help strings with new command names * clean contrib scripts * disable mmap on Windows * enhance darcs send message * fix quickcheck suite * shorter README
Categories: Offsite Discussion

Beginner: Art in Haskell

Haskell on Reddit - Mon, 11/09/2015 - 2:47pm

I was wondering if anyone had any links or advice when it came to doing art in Haskell.

I'm quite new to Haskell but wanted to try out some graphics stuff (fractals, etc).

Where would be a good place to start? :)

submitted by Catamorpheus
[link] [12 comments]
Categories: Incoming News

minElem function int -> intger -> double

Haskell on Reddit - Mon, 11/09/2015 - 1:18pm

Hi, if i have a function that searches the minimum element in the list with Int, how can i use it with Intger and double?

thx 4 help

submitted by mohawke781
[link] [8 comments]
Categories: Incoming News

Leuven Haskell User Group: Season 2

General haskell list - Mon, 11/09/2015 - 1:07pm
Dear Haskellers, Season 2 of the Leuven Haskell User Group starts on November 17. Join us for an introductory talk on type classes. Everyone is welcome. For more information:!forum/leuven-haskell See you there!
Categories: Incoming News

Permutation differnce

Haskell on Reddit - Mon, 11/09/2015 - 12:59pm

Hi guys, can you help me finding the differnce between

import Data.List permHH [] = [[]] permHH [a] = [[a]] permHH as = [x:xs | x <- nub as, xs <- permHH (delete x as)]


permLL [] = [[]] permLL as = [as!!(i-1):xs | i <- [1..length as], xs <- permLL (take (i-1) as ++ drop i as)]

i get the same results for both functions, but there has to be a difference.

thx for helping

submitted by mohawke781
[link] [comment]
Categories: Incoming News

Does this happen to anyone else: I mention Haskell to somebody I meet, and they hear Pascal.

Haskell on Reddit - Mon, 11/09/2015 - 7:36am

So instead of revealing something somewhat novel and interesting, I reveal boring and antiquated until I can correct them.

submitted by zzing
[link] [146 comments]
Categories: Incoming News

Anybody using the "top-down" cabal-install solver?

haskell-cafe - Mon, 11/09/2015 - 7:18am
(Sorry if you get this twice, forgot to cross-post to -cafe initially.) Hi all, Just to get input from as many people as possible: I was pondering a plan for modularizing[2] the Cabal solver[1] and wanted to reach as many people as possible with my question: Is anybody is still using the top-down solver? Please respond to this list if you are, especially if you're doing so because there's no other way to get the modular solver to do what you want. (Obviously, I'm not promising to fix any problems you may have with the modular solver, but it would be valuable information since it could affect the decision of whether we have to keep the top-down solver around.) Regards, -- [1] [2] "Splitting it out into its own library" is perhaps a more accurate description, but somewhat unwieldly :).
Categories: Offsite Discussion

Eric Kidd: Bare Metal Rust: Low-level CPU I/O ports

Planet Haskell - Mon, 11/09/2015 - 6:33am

Want to build your own kernel in Rust? See the Bare Metal Rust page for more resources and more posts in this series.

Rust is a really fun language: It allows me to work on low-level kernel code, but it also allows me to wrap my code up in clean, high-level APIs. If you this sounds interesting, you should really check out Philipp Oppermann's blog posts about writing a basic x86_64 operating system kernel in Rust. He walks you through booting the kernel, entering long mode, getting Rust running, and printing text to the screen.

Once you get a basic kernel running, you'll probably want to start working on basic I/O, which requires interrupts. And this point, you'll find that pretty much every tutorial dives right into the in and out instructions. For example, if you look at the introduction to interrupts, the very first code you'll see is (comments added):

mov al,20h ; Move interrupt acknowledgment code into al. out 20h,al ; Write al to PIC on port 0x20.

Here, we're talking to the PIC ("Programmable Interrupt Controller"), and we're telling it that we've finished handling a processor interrupt. To do this, we need to write an 8-bit status code to the I/O port at address 0x20.

Traditionally, we would wrap this up in an outb ("out byte") function, which might look something like this in Rust:

// The asm! macro requires a nightly build of Rust, and // we need to opt-in explicitly. #![feature(asm)] unsafe fn outb(value: u8, port: u16) { asm!("outb %al, %dx" :: "{dx}"(port), "{al}"(value) :: "volatile"); }

This writes an 8-byte value to the specified port. It uses the unstable Rust extension asm!, which allows us to use GCC/LLVM-style inline assembly. We'd invoke it like this:

outb(0x20, 0x20);

But let's see if we can wrap a higher-level API around an I/O port.

Read more…

Categories: Offsite Blogs