Skip to content

Instantly share code, notes, and snippets.

@eduardoleon
Created December 17, 2014 11:04
Show Gist options
  • Save eduardoleon/778ea5293d315153ffd2 to your computer and use it in GitHub Desktop.
Save eduardoleon/778ea5293d315153ffd2 to your computer and use it in GitHub Desktop.
Polytypic programming using GADTs
{-# 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]
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 ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment