emilaxelsson

{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}

{-# OPTIONS_GHC -Wall                        #-}
{-# OPTIONS_GHC -Wno-missing-signatures      #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}

{-

Setup and start Gremlin server:

emilaxelsson

{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE OverloadedLabels           #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE Rank2Types                 #-}

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);
}

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

s{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

-- A version of the code from <http://fun-discoveries.blogspot.se/2016/03/compilation-as-typed-edsl-to-edsl.html>
-- which avoids incomplete matching on `Val` and `Ref`.

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

  <!--
\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

  <!--
\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

 > [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

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