edsko

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE EmptyCase             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}

edsko

import Control.Applicative
import Control.Monad
import Control.Monad.IO.Class
import System.IO.Unsafe

newtype LazyIO a = LazyIO { runLazyIO :: IO a }

instance Monad LazyIO where
  return a = LazyIO (return a)
  LazyIO x >>= f = LazyIO $ unsafeInterleaveIO $ x >>= runLazyIO . f

edsko

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

edsko

{-------------------------------------------------------------------------------
  Lazy n-ary cartesian product

  Most of these functions (except for 'cart' itself) are taken from
  "Generics.Deriving.Enum", which in turn are taken from Mark Jones' talk
  at AFP 2008.
-------------------------------------------------------------------------------}

-- | n-ary lazy cartesian product
ncart :: HList [] as -> [HList Identity as]

edsko

data Strategy = Concat

(+++) :: [a] -> [a] -> Strategy -> [a]
(+++) xs ys Concat = xs ++ ys

(.@) :: (Strategy -> a) -> Strategy -> a
(.@) = ($)

test :: [Int]
test = [1] +++ [2] .@ Concat

edsko

{-@ data List [listLen] a = Nil | Cons { hd :: a , tl :: List a } @-}
data List a = Nil | Cons a (List a)

{-@ measure listLen @-}
{-@ listLen :: List a -> Nat @-}
listLen :: List a -> Int
listLen Nil        = 0
listLen (Cons _ cs) = 1 + listLen cs

edsko

repeatedly :: (a -> b -> b) -> ([a] -> b -> b)
repeatedly = flip . foldl' . flip

repeatedlyM :: Monad m => (a -> b -> m b) -> ([a] -> b -> m b)
repeatedlyM = flip . foldlM' . flip

foldlM' :: forall m a b. Monad m => (b -> a -> m b) -> b -> [a] -> m b
foldlM' f e = go e
  where
    go :: b -> [a] -> m b

edsko

type family Repeat (n :: Nat) (a :: *) :: [*] where
  Repeat 'Zero     a = '[]
  Repeat ('Succ n) a = a ': Repeat n a

fromHomSum :: SNat n -> NS f (Repeat n a) -> f a
fromHomSum SZero     ns     = case ns of {}
fromHomSum (SSucc _) (Z a)  = a
fromHomSum (SSucc n) (S as) = fromHomSum n as

toHomProd :: [f a] -> (forall n. SListI (Repeat n a) => SNat n -> NP f (Repeat n a) -> b) -> b

edsko

module Blog where

import Prelude hiding ((.), id)
import Control.Category
import Data.Bifunctor

{-------------------------------------------------------------------------------
  Fixed points
-------------------------------------------------------------------------------}

edsko

{-# LANGUAGE GADTs              #-}
{-# LANGUAGE StandaloneDeriving #-}

{-# OPTIONS_GHC -Wall -fno-warn-incomplete-patterns #-}

module HdWalletNotes where

{-------------------------------------------------------------------------------
  This module is a simple Haskell model of BIP-32, with a focus on why and
  how hardening works. We start with some types for which we need no further