Skip to content

Instantly share code, notes, and snippets.

@michaelpj
michaelpj / MutualFix.agda
Last active January 6, 2019 15:52 — forked from effectfully/MutualFix.agda
Mutual term-level recursion
{-# OPTIONS --type-in-type #-}
fstFun : ∀ {A B} -> A -> B -> A
fstFun x _ = x
sndFun : ∀ {A B} -> A -> B -> B
sndFun _ y = y
uncurryFun : ∀ {A B C} -> (A -> B -> C) -> (∀ {R} -> (A -> B -> R) -> R) -> C
uncurryFun f k = f (k fstFun) (k sndFun)
@michaelpj
michaelpj / Playground.hs
Created February 4, 2019 16:38
Plutus Playground Smart Contract
-- | Vesting scheme as a PLC contract
module Vesting where
import Control.Monad (void)
import qualified Language.PlutusTx as PlutusTx
import qualified Ledger.Interval as Interval
import qualified Language.PlutusTx.Prelude as P
import Ledger
import Ledger.Ada (Ada)
@michaelpj
michaelpj / Example.hs
Last active July 31, 2019 15:25
Forgetting the types on a mapped HList
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
cradle:
multi:
- path: ./.
config:
cradle:
cabal:
- path: ./.
config:
cradle:
cabal:
@michaelpj
michaelpj / test.nix
Created June 16, 2020 14:16
Ormolu haskell.nix
{ pkgs ? import ./nixpkgs.nix
, haskellCompiler ? "ghc865"
}:
let
haskellNix = import (builtins.fetchTarball
( "https://github.com/input-output-hk/haskell.nix/archive/"
+ "59cf05606e7efbbc4741ae28fd8cc610cec94eb8.tar.gz"
)) {};
nixpkgsSrc = haskellNix.sources.nixpkgs-default;
@michaelpj
michaelpj / Traversable1.hs
Created September 21, 2021 10:44
Easy Traversable1 instances
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
module Traversable1 where
import Data.Functor.Apply
import Data.Semigroup.Foldable
import Data.Semigroup.Traversable
-- | Apply a non-empty container of functions to a possibly-empty-with-unit container of values.
(<.*>) :: (Apply f) => f (a -> b) -> MaybeApply f a -> f b
-- A stateful funciton with a counter and a boolean saying if it has terminated
-- We use bracket to always set the termination boolean, even if there is an exception
-- in the initial action.
ghci> let f st act =
bracket
(pure ())
(\_ -> modify st (\(c,fin) -> (c, True)))
(\_ -> do { act; modify st (\(c, fin) -> ((c + 1), fin)) })
ghci> :t f
f :: (st :> es, Num a1) =>