Skip to content

Instantly share code, notes, and snippets.

@anka-213
Created November 19, 2018 15:08
Show Gist options
  • Save anka-213/95eeb79d5df196dc196f93f96d1d27c9 to your computer and use it in GitHub Desktop.
Save anka-213/95eeb79d5df196dc196f93f96d1d27c9 to your computer and use it in GitHub Desktop.
A module for converting functions into concrete algebraic data structures
{- |
This module gives a direct representation of concrete functions as
algebraic data structures.
> show not
>>> (False => True) :++: (True => False)
> show (&&)
>>> (False => ((False => False) :++: (True => False)))
:++: (True => ((False => False) :++: (True => True )))
> show (succ :: Nat -> Nat)
>>> (Zero => 1) :++: (Suc => ((Zero => 2) :++: (Suc => ((Zero => 3) :++: (Suc => ((Zero => 4) :++: (Suc => ((Zero => 5) :++: (Suc => ((Zero => 6) :++: (Suc => ((Zero => 7) :++: (Suc => ((Zero => 8) :++: (Suc => ((Zero => 9) :++: (Suc => ((Zero => 10) :++: (Suc => ((Zero => 11) :++: (Suc => ((Zero => 12) :++: (Suc => ((Zero => 13) :++: (Suc => ((Zero => 14) :++: (Suc => ((Zero => 15) :++: (Suc => ((Zero => 16) :++: (Suc => ((Zero => 17) :++: (Suc => ((Zero => 18) :++: (Suc => ((Zero => 19) :++: ...
> show (take 3 :: [()] -> [()])
>>> ([] => []) :++: (: => Curried (() => (([] => [()]) :++: (: => Curried (() => (([] => [(),()]) :++: (: => Curried (() => (([] => [(),(),()]) :++: (: => Curried (() => (([] => [(),(),()]) :++: ...
> take 3 :: [Void] -> [Void]
>>> ([] => []) :++: (: => Uncurried EmptyCase)
Any domain based on algebraic data structures
or functions will work out of the box with (for example):
> deriving via Generically (a, b) instance (MemoFunction a, MemoFunction b) => MemoFunction (a, b)
Once you have an instance MemoFunction a, you can convert a function to the representation with
> mto :: (a -> b) -> MemRep a b
and convert back to a function with
> mfrom :: MemRep a b -> (a -> b)
You can also use the representation for showing functions as an enumeration of all possible inputs.
This module exports an (orphan) instance for that:
> instance (MemoFunction a, Show (MemRep a b)) => Show (a -> b)
If the domain is infinite, the printed version of the function will also be infinite (except that this
module trucates long outputs by default).
For example, MemRep Nat a = Stream a
MemRep Bool a = Pair a
----
If your data-type is not algebraic, you will have to create the instance for MemoFunction by hand.
For example, if you want an instance for Int, you could convert it to a list of digits and
derive the instance for the converted version automatically, or you could define the tree structure
manually.
-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
-- {-# OPTIONS_GHC #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
--{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DerivingVia #-}
module MemoFunctions where
import GHC.Generics
import GHC.TypeLits hiding (Nat)
import Data.Proxy (Proxy(..))
-- | A class for automatic enumeration of functions.
-- If we have `MemoFunction a`, then `MemRep a b` is
-- a concrete representation (without functions) of
-- the function `a -> b`.
class MemoFunction a where
type MemRep a x
mto :: (a -> x) -> MemRep a x
mfrom :: MemRep a x -> (a -> x)
-- | Printing functions can often yield infinite results,
-- so we limit the length to some resonable amount.
limitShowsPrec :: Show a => Int -> a -> ShowS
limitShowsPrec n f = take 500 . showsPrec n f
-- | One key result of this file: a Show instance for functions.
instance (MemoFunction a, Show (MemRep a b)) => Show (a -> b) where
showsPrec n f = limitShowsPrec n (mto f)
instance (MemoFunction a, MemoFunction (MemRep a b)) => MemoFunction (a -> b) where
type MemRep (a -> b) x = MemRep (MemRep a b) x
mto f = mto (f . mfrom)
-- mto f = let f' = f . mfrom @a in MFun $ mto f'
mfrom (f) a = mfrom f (mto a)
-- deriving instance (Show (MemRep (MemRep a b) x)) => Show (MemRep (a -> b) x)
-- instance (Generic a, GMemoFunction (Rep a), MemoFunction (GMemRep (Rep a) b)) => MemoFunction (a -> b) where
-- type MemRep (a -> b) x = MemRep (GMemRep (Rep a) b) x
-- mto f = let f' = f . (. from) . gmfrom in MFun $ mto f'
-- mfrom (MFun f) a = mfrom f (gmto (a . to))
-- deriving instance (Show (MemRep (GMemRep (Rep a) b) x)) => Show (MemRep (a -> b) x)
-- * Generics
newtype Generically a = Generically { getGenerically :: a} -- deriving Functor
-- deriving newtype Show
instance (Generic a, GMemoFunction (Rep a)) => MemoFunction (Generically a) where
type MemRep (Generically a) x = GMemRep (Rep a) x
mto :: (Generically a -> x) -> MemRep (Generically a) x
mto f = gmto $ f . Generically . to
mfrom :: MemRep (Generically a) x -> Generically a -> x
mfrom f (Generically a) = gmfrom f (from a)
-- deriving instance Show (GMemRep (Rep a) x) => Show (MemRep (Generically a) x)
instance (Show a) => Show (Generically a) where
showsPrec n f = limitShowsPrec n f
-- | Automatic instances via generics.
--
-- > deriving via Generically Bool instance MemoFunction Bool
class GMemoFunction (f :: * -> *) where
data GMemRep f x
gmto :: (f p -> x) -> GMemRep f x
gmfrom :: GMemRep f x -> (f p -> x)
deriving newtype instance MemoFunction (GMemRep f x) => MemoFunction (GMemRep (S1 c f) x)
deriving newtype instance MemoFunction (GMemRep f x) => MemoFunction (GMemRep (D1 c f) x)
deriving newtype instance MemoFunction (GMemRep f x) => MemoFunction (GMemRep (C1 c f) x)
deriving newtype instance MemoFunction (GMemRep f (GMemRep g x)) => MemoFunction (GMemRep (f :*: g) x)
deriving newtype instance MemoFunction (MemRep f x) => MemoFunction (GMemRep (K1 c f) x)
deriving newtype instance MemoFunction x => MemoFunction (GMemRep U1 x)
-- deriving newtype instance MemoFunction a => MemoFunction (ConstrTag m a)
-- deriving via Generically (GMemRep (D1 c f) x) instance MemoFunction (GMemRep f x) => MemoFunction (GMemRep (D1 c f) x)
deriving via Generically (ConstrTag m a) instance MemoFunction a => MemoFunction (ConstrTag m a)
-- deriving via Generically (GMemRep (C1 c f) x) instance MemoFunction (GMemRep f x) => MemoFunction (GMemRep (C1 c f) x)
-- deriving via Generically (GMemRep (S1 c f) x) instance MemoFunction (GMemRep f x) => MemoFunction (GMemRep (S1 c f) x)
-- deriving via Generically (GMemRep U1 x) instance MemoFunction x => MemoFunction (GMemRep U1 x)
deriving via Generically (GMemRep V1 x) instance () => MemoFunction (GMemRep V1 x)
-- deriving via Generically (GMemRep (K1 c f) x) instance MemoFunction (MemRep f x) => MemoFunction (GMemRep (K1 c f) x)
deriving via Generically (GMemRep (f :+: g) x) instance (MemoFunction (GMemRep f x), MemoFunction (GMemRep g x)) => MemoFunction (GMemRep (f :+: g) x)
-- deriving via Generically (GMemRep (f :*: g) x) instance MemoFunction (GMemRep f (GMemRep g x)) => MemoFunction (GMemRep (f :*: g) x)
-- | Meta-data: Data structure. Ignored
instance GMemoFunction f => GMemoFunction (D1 c f) where
newtype GMemRep (D1 c f) x = MD1 (GMemRep f x) deriving Generic
-- gmto :: (D1 c f p -> x) -> GMemRep f x
gmto f = MD1 . gmto $ f . M1
-- gmfrom :: GMemRep f x -> D1 c f p -> x
gmfrom (MD1 f) (M1 a) = gmfrom f a
deriving newtype instance Show (GMemRep f x) => Show (GMemRep (D1 c f) x)
data ConstrTag (meta :: Meta) a = ConstrTag a deriving Generic
-- data ConstrTag meta a = ConstrTag a
-- Show which constructor maps to which value
instance forall name a i j. (KnownSymbol name, Show a) => Show (ConstrTag (MetaCons name i j) a) where
showsPrec n (ConstrTag f) = (("(" ++ symbolVal @name Proxy ++ " => ") ++) . limitShowsPrec n f . (")"++)
-- | Meta-data: Constructor
instance GMemoFunction f => GMemoFunction (C1 c f) where
newtype GMemRep (C1 c f) x = MC1 (ConstrTag c (GMemRep f x)) deriving Generic -- deriving newtype Show
-- gmto :: (C1 c f p -> x) -> ConstrTag c (GMemRep f x)
gmto f = MC1 . ConstrTag . gmto $ f . M1
-- gmfrom :: ConstrTag c (GMemRep f x) -> C1 c f p -> x
gmfrom (MC1 (ConstrTag f)) (M1 a) = gmfrom f a
deriving newtype instance (KnownSymbol name, Show (GMemRep f x)) => Show (GMemRep (C1 (MetaCons name fix sels) f) x)
-- Meta data: selector
instance GMemoFunction f => GMemoFunction (S1 c f) where
newtype GMemRep (S1 c f) x = MS1 (GMemRep f x) deriving Generic -- deriving newtype Show
-- gmto :: (S1 c f p -> x) -> GMemRep f x
gmto f = MS1 . gmto $ f . M1
-- gmfrom :: GMemRep f x -> S1 c f p -> x
gmfrom (MS1 f) (M1 a) = gmfrom f a
deriving newtype instance Show (GMemRep f x) => Show (GMemRep (S1 c f) x)
-- Unit case: a^1 == a
instance GMemoFunction U1 where
newtype GMemRep U1 x = MU1 x deriving Generic
-- gmto :: (U1 p -> x) -> GMemRep f x
gmto f = MU1 $ f U1
-- gmfrom :: GMemRep f x -> U1 p -> x
gmfrom (MU1 f) = const f
deriving newtype instance Show x => Show (GMemRep U1 x)
-- Empty case: a^0 == 1
instance GMemoFunction V1 where
data GMemRep V1 x = EmptyCase deriving Show deriving Generic
gmto _ = EmptyCase
gmfrom x v = case v of
-- Constant. Delegate to next level.
instance MemoFunction c => GMemoFunction (K1 i c) where
newtype GMemRep (K1 i c) x = MK1 (MemRep c x) deriving Generic
gmto f = MK1 . mto $ f . K1
gmfrom (MK1 f) a = mfrom f (unK1 a)
deriving newtype instance Show (MemRep c x) => Show (GMemRep (K1 i c) x)
-- Sum case: x^(a+b) = x^a + x^b
instance (GMemoFunction f, GMemoFunction g) => GMemoFunction (f :+: g) where
data GMemRep (f :+: g) x = GMemRep f x :++: GMemRep g x deriving Generic
gmto f = gmto (f . L1) :++: gmto (f . R1)
gmfrom ~(f1 :++: f2) (L1 a1) = gmfrom f1 a1
gmfrom ~(f1 :++: f2) (R1 a2) = gmfrom f2 a2
deriving instance (Show (GMemRep a x), Show (GMemRep b x)) => Show (GMemRep (a :+: b) x)
-- | Product case: x^(a*b) = (x^b)^a
-- (a,b) -> x = a -> (b -> x)
instance forall f g. (GMemoFunction f, GMemoFunction g) => GMemoFunction (f :*: g) where
newtype GMemRep (f :*: g) x = Curried (GMemRep f (GMemRep g x)) deriving Generic
gmto :: forall x p. ((f :*: g) p -> x) -> GMemRep (f :*: g) x
gmto f = Curried $ gmto (gmto . (\a b -> f (a :*: b)))
gmfrom :: GMemRep (f :*: g) x -> (f :*: g) p -> x
gmfrom (Curried f) (a :*: b) = gmfrom (gmfrom f a) b
deriving instance Show (GMemRep a (GMemRep b x)) => Show (GMemRep (a :*: b) x)
-- instance MemoFunction (f :.: g) where
-- type MemRep (f :.: g) = (f :.: g)
-- mto = id
-- mfrom = id
-- instance GMemoFunction p => GMemoFunction (Par1 p) where
-- type GMemRep (Par1 p) x = GMemRep p x
-- gmto f = mto $ f . Par1
-- gmfrom f a = mfrom f (unPar1 a)
-- instance GMemoFunction (Rec1 f) where
-- data GMemRep (Rec1 f) = (Rec1 f)
-- gmto = id
-- gmfrom = id
----------------
-- * Examples --
----------------
deriving via Generically Void instance MemoFunction Void
deriving via Generically Nat instance MemoFunction Nat
deriving via Generically () instance MemoFunction ()
deriving via Generically Bool instance MemoFunction Bool
deriving via Generically (Maybe a) instance MemoFunction a => MemoFunction (Maybe a)
deriving via Generically (Either a b) instance (MemoFunction a, MemoFunction b) => MemoFunction (Either a b)
deriving via Generically (a, b) instance (MemoFunction a, MemoFunction b) => MemoFunction (a, b)
deriving via Generically (a, b, c) instance (MemoFunction a, MemoFunction b, MemoFunction c) => MemoFunction (a, b, c)
deriving via Generically [a] instance MemoFunction a => MemoFunction [a]
data Loop = Loop Loop deriving (Show, Generic)
deriving MemoFunction via (Generically Loop)
-- deriving via (Generically Loop) instance MemoFunction Loop
-- instance MemoFunction Loop where
-- type MemRep Loop x = (GMemRep (Rep Loop) x)
-- mto f = gmto $ f . to
-- mfrom f a = gmfrom f (from a)
data Nat = Zero | Suc Nat
deriving (Eq, Generic)
-- deriving Show
instance Show Nat where
showsPrec n = showsPrec n . fromEnum
instance Enum Nat where
succ = Suc
pred Zero = Zero
pred (Suc n) = n
toEnum n = iterate Suc Zero !! n
fromEnum = go 0
where go !n Zero = n
go !n (Suc m) = go (n+1) m
-- fromEnum Zero = 0
-- fromEnum (Suc n) = 1 + fromEnum n
instance Num Nat where
fromInteger = toEnum . fromInteger
n + m = toEnum $ fromEnum n + fromEnum m
n * m = toEnum $ fromEnum n * fromEnum m
abs = undefined
signum = undefined
negate = undefined
data Void deriving (Generic, Eq, Show)
--------------------------------------
-- Misc debugging utility functions --
--------------------------------------
-- | Usage:
-- :kind! Simplify (Rep Foo)
type family Simplify x where
Simplify (M1 i c f) = Simplify f
Simplify (f :+: g) = Simplify f :+: Simplify g
Simplify (f :*: g) = Simplify f :*: Simplify g
Simplify x = x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment