emilaxelsson

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits

emilaxelsson

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

emilaxelsson

 > [UPDATE, 2015-02-23: The post has been slightly updated based on comments by Edward Kmett.]

In trying to understand the [Bound library](http://hackage.haskell.org/package/bound), and in particular, its limitations (if any) in terms of expressiveness and efficiency. I will here try to implement a small subset of the [Feldspar](http://hackage.haskell.org/package/feldspar-language) EDSL using Bound.

DISCLAIMER: Statements in this text may very well reflect my misunderstandings rather than actual truths about Bound.

Note that I'm assuming basic familiarity with Bound. If you're not familiar with the library, see [its documentation](http://hackage.haskell.org/package/bound/docs/Bound.html).

I would be happy to receive feedback and hints for how to improve the code.

emilaxelsson

  <!--
\begin{code}
module Loop where
\end{code}
  -->

(This post is literate Haskell, [available here](https://gist.github.com/emilaxelsson/26658849e39918883ffe).)

I've always thought that strictness annotations can only turn terminating programs into non-terminating ones. Turns out that this isn't always the case. As always, `unsafePerformIO` changes things.

emilaxelsson

  <!--
\begin{code}
module SudokuSAT where
\end{code}
  -->

(This post is literate Haskell, [available here](https://gist.github.com/emilaxelsson/e15a3b72eef7468e5edf).)

Inspired by an [old(-ish) Galois post](https://galois.com/blog/2009/03/solving-sudoku-using-cryptol/) about using its SAT back end to solve sudokus, here is a similar sudoku solver written in Haskell using Koen Claessen's [SAT+ library](https://github.com/koengit/satplus).

emilaxelsson

(This post is literate Haskell, [available here](https://gist.github.com/emilaxelsson/81d2774f0c96750378bf).)

This post will show a trick for making it easier to work with terms representated as fixed-points of functors in Haskell. It is assumed that the reader is familiar with this representation.

First some extensions:

\begin{code}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

emilaxelsson

{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeOperators #-}

import Control.Monad.State
import Data.Foldable (Foldable)
import qualified Data.Foldable as Fold
import Data.Map (Map)
import qualified Data.Map as Map

emilaxelsson

Proposal for feldspar-language and feldspar-compiler.

Background

Tuples are currently compiled to structs whenever they are forced by a Syntax-overloaded function, such as condition or forLoop. In most cases, we would like to avoid the struct and just have the members as separate variables.

Consider the example

emilaxelsson

// This file demonstrates that if `tgmath.h` is included, it doesn't matter if
// `math.h` is also included and which order the include statements appear.

#include <stdio.h>
#include <tgmath.h>
#include <math.h>

int main() {
    printf("%.20f\n", sinf((float) 5.0));
    printf("%.20f\n", sin((double) 5.0));

emilaxelsson

#include <stdbool.h>
#include <stdint.h>
#include <stdio.h>
#include <string.h>
#include <tgmath.h>
#include <time.h>
void printTime(clock_t start, clock_t end)
{
    printf("CPU time (sec): %f\n", (double) (end - start) / CLOCKS_PER_SEC);
}