News aggregator

Dependent Types for Low-Level Programming

Lambda the Ultimate - Mon, 09/28/2015 - 7:58am

Dependent Types for Low-Level Programming by Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula:

In this paper, we describe the key principles of a dependent type system for low-level imperative languages. The major contributions of this work are (1) a sound type system that combines dependent types and mutation for variables and for heap-allocated structures in a more flexible way than before and (2) a technique for automatically inferring dependent types for local variables. We have applied these general principles to design Deputy, a dependent type system for C that allows the user to describe bounded pointers and tagged unions. Deputy has been used to annotate and check a number of real-world C programs.

A conceptually simple approach to verifying the safety of C programs, which proceeeds in 3 phases: 1. infer locals that hold pointer bounds, 2. flow-insensitive checking introduces runtime assertions using these locals, 3. flow-sensitive optimization that removes the assertions that it can prove always hold.

You're left with a program that ensures runtime safety with as few runtime checks as possible, and the resulting C program is compiled with gcc which can perform its own optimizations.

This work is from 2007, and the project grew into the Ivy language, which is a C dialect that is fully backwards compatible with C if you #include a small header file that includes the extensions.

It's application to C probably won't get much uptake at this point, but I can see this as a useful compiler plugin to verify unsafe Rust code.

Categories: Offsite Discussion

Monads for effects now available in classical imperative languages

Haskell on Reddit - Mon, 09/28/2015 - 5:12am

I think it's relatively fair to say that most code in, say, Java runs in some form of IO+Except transformer. We model these effects separately. Other monads such as State, Reader and Writer can be simulated in IO and can be seen as subsets of it. On the other hand there's the List/Logic monad that provides us with an effect that I haven't seen in any other language. You can of course do non-determinism in any language but I don't know any that allows you to use the same interface as writing normal code. What are other examples of such "interesting" monads?

Edit: sorry about the title. "Now" should be "not"

submitted by Darwin226
[link] [28 comments]
Categories: Incoming News

Fmap and Map for lists

haskell-cafe - Mon, 09/28/2015 - 2:11am
Does anyone have any idea why fmap (Functor map) and the list map are separate functions? I think it would make plenty sense for the Functor map to just be named map and have lists respond to that _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion

What kinds of errors do you find in your pure (non-I/O) code at run time?

Haskell on Reddit - Sun, 09/27/2015 - 9:53pm

It's generally accepted that it's a fair bit harder to introduce bugs into non-IO Haskell code, than it is to do so in imperative languages. Type systems and purity both play a role. Haskell prevents many types of bugs from even occurring, especially those caused by working with tangles of pointers to mutable objects and functions riddled with non-obvious side-effects.

I'm not so clear on how we might characterize the run time (not compile time) bugs that occur in non-IO Haskell functions. You could quickly come up with two broad categories:

  • Crash-inducing bugs (Non-termination, pattern match failure, stack overflows (which could also occur in correct code)).
  • Other "logic errors", i.e. a function always returns a value, but it may not be the value we expect.

I think it should be possible to break down these categories further. Thinking about bugs you've encountered in your own code, are there more specific ways you might categorize them? Here's three subcategories of "logic error" to start:

  • Misunderstanding the problem you are trying to solve, or the method of solution
  • Arguments specified in the wrong order (and code still type-checks)
  • Misunderstood operator precedence (and code still type-checks)
submitted by -ecl3ctic-
[link] [19 comments]
Categories: Incoming News

Constrain Symbol to contain only alphabeticcharacters

haskell-cafe - Sun, 09/27/2015 - 7:10pm
Hi Café, Is it possible to do this? I looked through the source for GHC.TypeLits on hackage but found no leads. Thanks for any help, Alex _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion

Vincent Hanquez: Combining Rust and Haskell

Planet Haskell - Sun, 09/27/2015 - 6:00pm

Rust is a pretty interesting language, in the area of C++ but more modern / better. The stated goal of rust are: “a systems programming language focused on three goals: safety, speed, and concurrency”. Combining Rust with Haskell could create some interesting use cases, and could replace use of C in some projects while providing a more high level and safer approach where Haskell cannot be used.

One of my reason for doing this, is that writing code targetting low-level features is simpler in Rust than Haskell. For example, writing inline assembly or some lowlevel OS routines. Also the performance of Rust is quite close to C++, and I could see this being useful in certain case where Haskell is not as optimised.

In this short tutorial, let’s call Rust functions from Haskell.

The Rust library

First we start with an hypothetical rust library that takes a value, print to console and return a value.

Our entry point in Rust is a simple rust_hello, in a src/ file:

#[no_mangle] pub extern fn rust_hello(v: i32) -> i32 { println!("Hello Rust World: {}", v); v+1 }

One of the key thing here is the presence of the no_mangle pragma, that allow exporting the name of the function as-is in the library we’re going to generate.

Rust uses Cargo to package library and executable, akin to Cabal for haskell. We can create the Cargo.toml for our test library:

[package] name = "hello" version = "0.0.1" authors = ["Vincent Hanquez <>"] [lib] name = "hello" crate-type = ["staticlib"]

The only special trick is that we ask Cargo to build a static library in the crate-type section, instead of the default rust lib (.rlib).

Haskell doesn’t know other calling / linking convention like C++ (yet) or Rust, which is why we need to go through those hoops.

We can now build with our Rust library with:

cargo build

If everything goes according to plan, you should end up with a target directory where you can find the libhello.a library.

The haskell part

Now the haskell part is really easy, as this point there’s no much difference than linking with some static C library; first we create a src/Main.hs:

{-# LANGUAGE ForeignFunctionInterface #-} module Main where import Foreign.C.Types foreign import ccall unsafe "rust_hello" rust_hello :: CInt -> IO CInt main = do v <- rust_hello 2901 putStrLn ("Rust returned: " ++ show v)

Nothing special if you’ve done some C bindings yourself, otherwise I suggest having a look at the FFI article.

we can try directly linking with ghc:

ghc -o hello-rust --make src/Main.hs -lhello -Ltarget/debug

and running:

$ ./hello-rust Hello Rust World: 2901 Rust returned: 2902

That achieve the goal above. From there we can polish things and add this to a cabal file:

name: hello-rust version: license: PublicDomain license-file: LICENSE author: Vincent Hanquez maintainer: category: System build-type: Simple cabal-version: >=1.10 extra-source-files: src/ executable hello-rust main-is: Main.hs other-extensions: ForeignFunctionInterface build-depends: base >=4.8 && <4.9 hs-source-dirs: src default-language: Haskell2010 extra-lib-dirs: target/release, target/debug extra-libraries: hello

Note: The target/release path is to support building with the -release flag of cargo build. by listing the target/release and then target/debug, it should allow you to pickup the release library in preference to the debug library. It can also create some confusion, and print a warning on my system when one of the directory is missing.

The missing step is either adding some pre-build rules to cabal Setup.hs to run cargo build, or some more elaborate build system, both which are left as exercice to the interested reader.

Where this could go

Going forward, this could lead to having another language from Haskell to target that is not as lowlevel as C, but offer stellar performance and more high level constructs (than C) without imposing any other runtime system. This is interesting where you need to complete some tasks that Haskell is not quite ready to handle (yet).

For example, a non exhaustive list:

  • Writing cryptographic bindings in rust&asm instead of C&asm
  • Heavily Vector-Optimised routines
  • Operating system routines (e.g. page table handling) for a hybrid and safer operating system kernel.
  • Servo embedding

Let me know in the comments anything else that might be of interests !

Categories: Offsite Blogs

A proposal: separate out some IO actions into a Runtime monad

Haskell on Reddit - Sun, 09/27/2015 - 3:51pm

After this recent discussion about using IO in testing, it emerged that there are two very different senses in which you can 'use IO' in Haskell. On the one hand, you can actually perform IO on files, the network, etc. On the other hand, you can just use non-IO-performing actions that happen to have the IO type, like forkIO and newIORef.

What if we split off those actions like the two I mentioned above and put them in their own type. Maybe it could be called Runtime or RT, to get at the idea that you aren't doing any impure actions outside the program, just within its runtime?

If you really wanted some more typesafety, but you also want to, for example, use IORefs for mocking external state, as the poster I linked to did, then you could use RT as your new base, instead of IO.

This is just spitballing - with the amount of code depending on those IO actions that I'd propose moving, I don't think this would be at all feasible. But it feels like the right thing to do, to me, and I wanted to see if anyone else agreed.

submitted by theonlycosmonaut
[link] [34 comments]
Categories: Incoming News

Solutions to Typeclassopedia Ex. 3.3.1?

haskell-cafe - Sun, 09/27/2015 - 3:33pm
Would anyone care to share their solution to exercise 3.3.1 in Typeclassopedia? Thanks, -db _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion

Is there a library for interactive command line editing

Haskell on Reddit - Sun, 09/27/2015 - 3:26pm


I'm looking for a library that deals with with interactive command line editing.

The goal is building a simple editor for a toy language I'm currently working on.

I looked into Yi but I couldn't find any hint of a specific library that is used for that. (I don't wanna fork Yii)

Thanks in advance for any help/hints.

submitted by squweez
[link] [6 comments]
Categories: Incoming News

How do I create an API from shared operations in my monad?

Haskell on Reddit - Sun, 09/27/2015 - 1:00pm

I'm writing a little game engine in Haskell, and I just figured out how to use the transformers library.

Unfortunately I'm not sure how to fix the manually enforced invariant and duplicated in the process function below:

import Prelude hiding (id) import qualified Data.Map as Map import Game.Objects -- | Including Id, Object (and its accessor "id"). import Control.Monad.Trans.RWS.Lazy type GameDimensions = (Int, Int) data GameOperation = Create Object | Update Object | Delete Id type GameModel = Map.Map Id Object type GameMessage = Maybe String -- | The type of monad game operations run in. Executed commands must -- record their constituent operations, if any, for dispersal to remote clients. type Game = RWS GameDimensions [GameOperation] GameModel GameMessage -- | The possible commands in the game. data Command = Enter Object | Exit Id -- | Processes game commands per game logic. process :: Command -> Game -- | Place an object in the game if it doesn't exist yet. process (Enter object) = do model <- get let exists = Map.member (id object) model updated = insert (id object) object model if exists then return $ Just "That object already exists." else put updated >> tell [Insert object] >> return Nothing -- | Remove an object from the game if it exists. process (Exit id) = do model <- get let exists = Map.member (id object) model updated = delete (id object) model if not exists then return $ Just "That object does not exist." else put updated >> tell [Delete (id object)] >> return Nothing

First, I'd like to make it impossible for process to update state and not tell the corresponding command correctly. How can I upgrade the monadic API to only support functions that bundle together a put and a tell for a particular operation?

Second, I'd like to make the exists boolean available in process whenever the command targets a specific object. How can I make functionality conditionally available based on the type of command being processed?

Thank you for any feedback. Please let me know if there's a way for me to improve the question or simplify the example.

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

is it possible to auto generate monad from template function?

Haskell on Reddit - Sun, 09/27/2015 - 8:21am

is it possible to auto generate monad from template function?

such as if there is a algebra library eval x+2x+y return 3x+y

if unknown polynomial f and g

to keep monad it, n map to n n -> n

definition * 1. (eval subs(x=n,subs(y=1, f))) = n * 2. (eval subs(x=n,subs(y=1, g))) = n

search or generate f and g from the definition above with monad random

submitted by haski2
[link] [4 comments]
Categories: Incoming News

which library for math can solve this system with haskell?

Haskell on Reddit - Sun, 09/27/2015 - 7:01am

which library for math can solve this system with haskell?

if no library, which math algorithm can solve this numerically?

xy + z = 5 xy+xz = 6 xy*z +x = 7

submitted by haski2
[link] [7 comments]
Categories: Incoming News

Could not find module `Graphics.Rendering.Cairo' and how to compile this example

Haskell on Reddit - Sun, 09/27/2015 - 6:28am

ghci have cairo, but sudo ghci do not have cairo my program below can only run in sudo ghci

import Graphics.Rendering.Chart.Easy import Graphics.Rendering.Chart.Backend.Cairo import Graphics.UI.Gtk --import Graphics.UI.Gtk.Layout.BackgroundContainer --import Graphics.UI.Gtk.Board.BoardLink import Graphics.UI.Gtk.Display.Image import Graphics.UI.Gtk.Gdk.Screen import System.Environment import Graphics.Rendering.Cairo

when run example got error in ghci (not sudo ghci)

[1 of 1] Compiling Main ( aa.hs, interpreted )

aa.hs:20:32: Couldn't match expected type ‘(a0 -> m0 a0) -> t0 -> IO Bool’ with actual type ‘IO ()’ The function ‘renderWithDrawable’ is applied to four arguments, but its type ‘DrawWindow -> Render () -> IO ()’ has only two In a stmt of a 'do' block: renderWithDrawable drawin myDraw return (eventSent x) In the expression: do { renderWithDrawable drawin myDraw return (eventSent x) }

aa.hs:20:73: Couldn't match expected type ‘Graphics.UI.Gtk.Gdk.Events.Event -> t0’ with actual type ‘Control.Monad.Trans.Reader.ReaderT (GHC.Ptr.Ptr any0) IO Bool’ The function ‘eventSent’ is applied to one argument, but its type ‘EventM any0 Bool’ has none In the fourth argument of ‘renderWithDrawable’, namely ‘(eventSent x)’ In a stmt of a 'do' block: renderWithDrawable drawin myDraw return (eventSent x) Failed, modules loaded: none.

submitted by haski2
[link] [1 comment]
Categories: Incoming News

how to solve library between sudo ghci and ghci in haskell

Haskell on Reddit - Sun, 09/27/2015 - 2:54am

some library must need sudo ghci in order to succeed to install

but some library must need to install with normal user mode, ghci

when i use with normal user mode ghci, i can not use the library which installed with sudo cabal install before

when run in sudo ghci mode, has error, only no error in normal user mode

*Main> let aa = splitOn " " "head tail [1,2,3]" *Main> let bb = filter (not . null) aa

<interactive>:21:22: Not in scope: `.'

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

There is no difference between using rev and not use rev and how to not specify the type when run eval from library plugins

Haskell on Reddit - Sun, 09/27/2015 - 2:41am

There is no difference between using rev and not use rev

*Main> rev mm!!1 ["[1,2,3]","head"] *Main> mm!!1 ["[1,2,3]","head"]

goal is to design a syntax which can run no matter how the statement split

reference from

choose n list = concatMap permutations $ choose' list [] where choose' [] r = if length r == n then [r] else [] choose' (xs) r | length r == n = [r] | otherwise = choose' xs (x:r) ++ choose' xs r

nondec :: Ord a => [a] -> Bool nondec xs = and (map leq (zip xs (tail xs))) where leq (x, y) = x <= y

foo xs = [(length xs-1), (length xs -2)..0] rev xs = [xs !! k| k <- foo xs]

let aa = splitOn " " "head tail [1,2,3]" let mm = filter nondec (choose (length aa -1) $ aa)

how to not specify the type when run eval from library plugins

*Main> eval "head [1,2,3] :: Int" [] :: IO (Maybe Int) Just 7 *Main> eval "head [1,2,3]" [] :: IO (Maybe Int)

<eval>:1:7: No instance for (Num a0) arising from the literal 1' The type variablea0' is ambiguous Possible fix: add a type signature that fixes these type variable(s) Note: there are several potential instances: instance Num Double -- Defined in GHC.Float' instance Num Float -- Defined inGHC.Float' instance Integral a => Num (GHC.Real.Ratio a) -- Defined in GHC.Real' 11 others In the expression: 1 In the first argument ofhead', namely `[1, 2, 3]' In the expression: head [1, 2, 3]

<eval>:1:19: No instance for (Typeable a0) arising from a use of toDyn' The type variablea0' is ambiguous Possible fix: add a type signature that fixes these type variable(s) Note: there are several potential instances: instance Typeable Dynamic -- Defined in Data.Dynamic' instance [overlap ok] Typeable () -- Defined inData.Typeable.Internal' instance [overlap ok] Typeable Bool -- Defined in Data.Typeable.Internal' 19 others In the expression: toDyn nws In the expression: let nws = head [...] in toDyn nws In an equation forresource': resource = let nws = head ... in toDyn nws Nothing

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