Aaron Levin aaronlevin

Recently had some trouble with nix. I was trying to write a Haskell ffi wrap around the micro-ecc lib. After doing this successfully, I wanted my library to work if micro-ecc was correctly installed somewhere on your system. I had the following two directories:

$ ls
micro-ecc
hs-micro-ecc

In micro-ecc I had a fairly vanilla nix expression that looked like:

	-- \| at the end of this post (http://aaronlevin.ca/post/106721413033/type-families-make-life-and-free-monads-simpler) I conjectured
	-- if it would be possible to expose the Free Crud monad as a library (for some definition of the term). Thanks to a huge help
	-- from @a_cowley, I think I'm converging on an idea. All the hard stuff was suggested to me by anthony!

	-- \| kitchen sink of extensions

	{-# LANGUAGE ConstraintKinds #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE FlexibleInstances #-}

	module freecrud

	-- \| a really crud(e) and naive attempt at porting over "dependently"-typed haskell code to idris.
	-- original haskell code here: https://gist.github.com/aaronlevin/437ceac6acc344f86ef9
	-- This is my first idris "program."

	-- \| crud lib

	data CrudVerb = Create \| Read

	# This template will give you a prompt with:
	# - ghc
	# - cabal
	# - ghc-mod
	# - the libraries: free, mtl, transformers
	#
	# to run: nix-shell haskell-project.nix
	#
	# to specify specific version of haskell, you can:
	# nix-shell --arg haskellPackages 'with import <nixpkgs> {}; haskellPackages_ghc783_profiling'

	-- \| playing around with a possible postgresql-simple plugin for servant

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE OverloadedStrings #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeOperators #-}

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeOperators #-}

	module FreeCrud where

	-- \| some user types

	-- \| I wanted to encode the json key for a payload type as type-level strings
	-- one can use equality constraints to resolve type family mappings

	data SomeData = SomeData

	type family Key (a :: *) :: Symbol where
	Key SomeData = "some_data"

	-- \| here we use equality constrains to resolve `k` to the type-level mapping
	-- of SomeData a. then we can restrict `k` to some other constraint (in this

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE OverloadedStrings #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE TypeFamilies #-}

	module Main where

	import Control.Monad
	import Data.Aeson
	import qualified Data.Aeson as A