Since version 7.10.1, GHC supports so-called type-checker plugins which let us extend GHC’s constraint solver, i.e. extend the the range of programs GHC can type check.
Several plugins have already been released, the ones I know are:
Adam Gundry’s uom-plugin: for supporting units of measure.
Iavor Diatchki’s type-nat-solver: which allows you to hook up SMT solvers to solve numeric constraints.
My own plugins:
ghc-typelits-natnormalise: which solves numeric constraints using a custom normalisation procedure as opposed to Iavor’s approach, which uses SMT solvers.
ghc-typelits-extra: which adds a type-level greatest common denominator (GCD) and (ceiling of) logarithm operator for GHCs type-level Natural numbers.
This post will be about writing our own type-checker plugin: we will build a plugin that (just like ghc-typelits-extra) allows GHC to perform GCD on types of kind Nat.
In this tutorial we’ll be programming the Terasic DE0-Nano FPGA development board using the functional hardware description language CλaSH.
The end result of this tutorial is demonstrated in the video below:
This tutorial is not a general introduction to CλaSH, nor to programming FPGAs.
It is meant to demonstrate how to use of TopEntity annotations (added in version 0.5.5 of CλaSH) to configure your CλaSH designs for an FPGA, without writing a single line of VHDL or (System)Verilog.
Even then, this tutorial is already almost too long for single blog post, but here goes:
Cabal 1.22 has preliminary support for relocatable packages, which is actually undocumented because I’m a bad patch writer.
Regardless, this preliminary support for relocatable packages partially enables relocatable sandboxes. What’s this partial part you might ask?
Well, only the .cabal-sandbox directory is relocatable, not the sandbox config file. So basically the part that takes the longest time to build is relocatable.
So, how do you go about the creating such a relocatable .cabal-sandboxdirectory? easy: