Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Basic Type-level Programming
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.