FiniteEndoTypes

FiniteEndoTypes.fm

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)