oisdk

import Data.Fin
import Data.Vect
import Prelude.WellFounded

%default total

data Tree : Nat -> Type -> Type where
  Leaf : Tree Z a
  Node : a -> (n : Nat) -> Tree n a -> Tree m a -> Tree (S (n + m)) a

oisdk

import Data.List
import GHC.Base (build)
import qualified Data.Set as Set
import Control.Monad.State
import Test.QuickCheck

toFact n = unfoldl (uncurry go) (n,1)
  where
    go 0 _ = Nothing
    go n m = case n `quotRem` m of

oisdk

{-# LANGUAGE DataKinds, UndecidableInstances, ConstraintKinds, GADTs, FlexibleInstances, EmptyCase, LambdaCase #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

import GHC.TypeLits

data Dict c where
  Dict :: c => Dict c

oisdk

{-# LANGUAGE BangPatterns #-}

module Seq (fmap',traverse') where

import Data.Coerce
import Control.Applicative (liftA2)

newtype Seq a = Seq { unSeq :: a }

instance Functor Seq where

oisdk

newtype Free c a = Free { runFree ∷ ∀ b. c b ⇒ (a → b) → b }

type (a ∷ k → Constraint) ⊨ (b ∷ k → Constraint) = (∀ x. a x ⇒ b x ∷ Constraint)

instance (Monoid ⊨ c) ⇒ Foldable (Free c) where
    foldMap = flip runFree

ala ∷ (∀ x. c x ⇒ c (f x), ∀ x. Coercible x (f x)) ⇒ Free c a → (∀ x. x → f x) → Free c a
ala xs to = Free (\k → coerce (runFree xs (to #. k)))

oisdk

{-# LANGUAGE BangPatterns #-}

import System.Random
import GHC.Base (oneShot)

choose :: (Foldable f, RandomGen g) =>  f a -> g -> (Maybe a, g)
choose xs = foldr f (const (,)) xs (0 :: Integer) Nothing
  where
    f x a = oneShot (\ !c m g -> case m of 
      Nothing -> a 1 (Just x) g

oisdk

import Data.Tree

-- | Lists of nodes at each level of the tree.
levels :: Tree a -> [[a]]
levels (Node x xs) = [x] : levelsForest xs

-- | Lists of nodes at each level of the forest.
levelsForest :: Forest a -> [[a]]
levelsForest ts = foldl f b ts [] []
  where

oisdk

import qualified Data.Tree           as Rose

data Tree a
    = Leaf Int a
    | Node [Tree a]
    deriving (Show,Eq,Functor)

-- | Given a nondeterministic, commutative binary operator, and a list
-- of inputs, enumerate all possible applications of the operator to
-- all inputs, without recalculating subtrees.

oisdk

{-# LANGUAGE RecursiveDo #-}

import qualified Data.Map.Strict as Map
import Control.Monad.State.Strict

repMax :: (Traversable t, Ord a) => t a -> t a
repMax xs = flip evalState Nothing $ mdo
  ys <- forM xs $ \x -> do
    modify (max (Just x))
    pure (max x res)

oisdk

{-# LANGUAGE TypeOperators, TypeFamilies, EmptyCase, DefaultSignatures, FlexibleContexts, UndecidableInstances, ScopedTypeVariables, DeriveGeneric #-}

import GHC.Generics
import Data.Proxy
import Prelude hiding (take)
import Data.Void

class Summable c where
  type Sum c a r :: *
  take :: c p -> (a -> r) -> Sum c a r