Polytypic programming using GADTs

GADT.hs

{-# LANGUAGE GADTs #-}

import Control.Arrow

data Sized a where
  Unit ::                        Sized ()
  Int  ::                        Sized Int
  Char ::                        Sized Char
  Sum  :: Sized a -> Sized b  -> Sized (Either a b)
  Prod :: Sized a -> Sized b  -> Sized (a, b)
  Iso  :: Sized a -> (b -> a) -> Sized b

size :: Sized a -> a -> Int
size  Unit      = const 0
size  Int       = const 1
size  Char      = const 1
size (Sum  f g) = size f ||| size g
size (Prod f g) = size f *** size g >>> uncurry (+)
size (Iso  f g) = size f . g

conv []     = Left  ()
conv (x:xs) = Right (x, xs)

list f = g
  where
    g = Iso h conv
    h = Sum Unit $ Prod f g

main = print $ list Int `size` [1..5]

GADT.ml

type ('a, 'b) either =
  | Left  of 'a
  | Right of 'b

let either f g = function
  | Left  x -> f x
  | Right y -> g y

let both f g h (x, y) = f (g x) (h y)

type 'a sized =
  | Unit :                          unit            sized
  | Int  :                          int             sized
  | Char :                          char            sized
  | Sum  : 'a sized * 'b sized   -> ('a, 'b) either sized
  | Prod : 'a sized * 'b sized   -> ('a * 'b)       sized
  | Iso  : 'a sized * ('b -> 'a) -> 'b              sized

let const x _ = x

let rec size : type a. a sized -> a -> int = fun f x ->
  match f with
  | Unit        -> 0
  | Int         -> 1
  | Char        -> 1
  | Sum  (f, g) -> either   (size f) (size g) x
  | Prod (f, g) -> both (+) (size f) (size g) x
  | Iso  (f, g) -> size f (g x)

let conv = function
  | []      -> Left  ()
  | x :: xs -> Right (x, xs)

let list f =
  let rec g = Iso (h, conv)
      and h = Sum (Unit, Prod (f, g))
  in g;;

print_int (size (list Int) [1;2;3;4;5]);
print_newline ()