Created
November 19, 2018 15:08
-
-
Save anka-213/95eeb79d5df196dc196f93f96d1d27c9 to your computer and use it in GitHub Desktop.
A module for converting functions into concrete algebraic data structures
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- | | |
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