robrix

module Data.FoldableN where

import Control.Applicative -- for ZipList
import Linear.V1 -- for V1, an identity functor
import Linear.V2 -- for V2, data V2 a = V2 a a

class Foldable t => FoldableN t where
  -- | Fold multiple structures into a 'Monoid'.
  --
  -- @

robrix

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
module NNat where

robrix

compile: input file benchmark/Send/Send10.hs
*** Checking old interface for Send.Send10 (use -ddump-hi-diffs for more details):
*** Parser [Send.Send10]:
!!! Parser [Send.Send10]: finished in 0.55 milliseconds, allocated 0.957 megabytes
*** Renamer/typechecker [Send.Send10]:
!!! Renamer/typechecker [Send.Send10]: finished in 186.13 milliseconds, allocated 77.516 megabytes
*** Desugar [Send.Send10]:
Result size of Desugar (before optimization)
  = {terms: 195, types: 4,554, coercions: 6,170, joins: 0/7}
Result size of Desugar (after optimization)

robrix

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, DefaultSignatures, DeriveAnyClass, DeriveFunctor, DeriveGeneric, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators #-}
module Rollable where

import Data.Functor.Foldable
import GHC.Generics

data Tree = Empty | Node Tree Int Tree
  deriving (Eq, Generic, Ord, Rollable, Show)

depth :: Tree -> Int

robrix

module ParameterizedRecursion where

import Data.Function

-- A recursive function…
showTable :: (Show a, Show b) => [(a, b)] -> String
showTable ((a, b) : rest) = show a ++ " | " ++ show b ++ "\n" ++ showTable rest
showTable [] = ""

-- …can be defined instead as a fixpoint…

robrix

dyna :: Functor f => (f (Cofree f a) -> a) -> (c -> f c) -> c -> a
dyna a c = extract . h
  where h = cofree . uncurry (:<) . (a &&& identity) . fmap h . c

ses :: Eq a => [a] -> [a] -> [These a a]
ses as bs = dyna (selectBest . edges (length as)) (editGraph as) (as, bs)

-- | A vertex in the edit graph.
data Vertex a x = Vertex { xs :: [a], ys :: [a], next :: Maybe x }
  deriving (Eq, Functor, Show)

robrix

{-# LANGUAGE DefaultSignatures, DeriveAnyClass, StandaloneDeriving, TypeFamilies, TypeOperators #-}
module Constructor where

import Data.Function (on)
import GHC.Generics
import Prologue

-- | The class of types for which we can determine whether an inhabitant was constructed with some specific constructor.
--
--   Note that the provided instance for functions returning 'HasConstructor' types, @HasConstructor b => HasConstructor (a -> b)@, applies its first argument to 'undefined'. Thus, data types with strict fields cannot safely implement 'HasConstructor' instances, since they would diverge. If you really want to play with fire, then you’ll have to apply the constructors to any strict fields yourself on the left-hand side.

robrix

{-# LANGUAGE DeriveFunctor #-}
module Bidi where

-- For 'guard'.
import Control.Monad
-- We use Cofree to represent type-annotated terms.
import Control.Comonad.Cofree
import Data.Functor.Classes
-- We use Fix to represent unannotated terms.
import Data.Functor.Foldable

robrix

import Data.Maybe
import Data.Monoid

-- | Join a Foldable collection of Monoids by a separator element.
join :: (Monoid a, Foldable t) => a -> t a -> a
join sep = fromMaybe mempty . fst . foldr combine (Nothing, True)
  where combine each (into, isFirst) = if isFirst
                                       then (Just each, False)
                                       else (Just each <> Just sep <> into, False)

robrix

Higgledy piggledy
parametricity’s
quite a nice property
functions can use;

Enforcing the absence of
state or identity
up to the type level
promotes reuse.