Skip to content

Instantly share code, notes, and snippets.

@johnchandlerburnham
Last active April 15, 2020 13:55
Show Gist options
  • Save johnchandlerburnham/fe53c5702bca6f0925f344905e82c0b0 to your computer and use it in GitHub Desktop.
Save johnchandlerburnham/fe53c5702bca6f0925f344905e82c0b0 to your computer and use it in GitHub Desktop.
FiniteEndoTypes
module FiniteEndoTypes where
import System.IO
-- for any finite n, there are n^n mappings from the set with n elements to
-- itself
-- for n == 2
-- {0,1} -> {0,0} 0
-- {0,1} -> {0,1} 1
-- {0,1} -> {1,0} 2
-- {0,1} -> {1,1} 3
-- these can be numbered by ordering the domain and interpreting the image as base n digits
mkEndoType :: Int -> Int -> String
mkEndoType n fn = concat
[ typ," : Type\n"
, " ", slf, "\n"
, all
, " P(" ++ typ ++ "_value)"
, "\n"
, vals
, "\n"
]
where
typ = "N" ++ show n ++ "." ++ show fn
slf = typ ++ "_value<P: " ++ typ ++ " -> Type> ->"
var i = "n" ++ show n ++ "." ++ show fn ++ ".v" ++ show i
all = concat $ (\i -> " P(" ++ var i ++ ") -> \n") <$> [0..(n - 1)]
lam = concat $ (\i -> "(x" ++ show i ++ ") ") <$> [0..(n - 1)]
val [] [] = ""
val (i:is) (x:xs) = concat
[ var i," : ",typ,"\n"
, " <P> ",lam,"x",show x,"\n"
, val is xs
]
vals = val [0..(n - 1)] (reverse $ toBaseDigits fn n)
toBaseDigits :: Int -> Int -> [Int]
toBaseDigits x b = go x b 0
where
go x b n = if n == b then [] else let (r,d) = divMod x b in d:(go r b (n+1))
mkAllEndoTypes :: Int -> String
mkAllEndoTypes n = concat $ mkEndoType n <$> [0..(n^n - 1)]
writeEndo :: Int -> FilePath -> IO ()
writeEndo n file = do
writeFile file (mkAllEndoTypes n)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment