Basic Type-level Programming

basic-type-level-programming.hs

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

import Prelude hiding (product, sum)

import Data.Proxy
import GHC.TypeLits

data Nil
data Cons x xs

class Sum list x | list -> x where
  sum :: Proxy list -> Proxy x
  sum _ = Proxy
instance Sum Nil 0
instance (Sum rest n2, n ~ (n1 + n2)) => Sum (Cons n1 rest) n

sum123 :: Proxy 6
sum123 = sum (Proxy :: Proxy (Cons 1 (Cons 2 (Cons 3 Nil))))

class Product list x | list -> x where
  product :: Proxy list -> Proxy x
  product _ = Proxy
instance Product Nil 1
instance (Product rest n2, n ~ (n1 * n2)) => Product (Cons n1 rest) n

problem1 :: forall (n :: Nat). Proxy (Cons n Nil) -> Proxy n
problem1 = sum

problem2 :: Proxy (Cons 2 (Cons 3 (Cons 4 Nil))) -> Proxy 24
problem2 = product