DataKinds / Proxy Assignment

Assignment.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Proxy where

import Data.Proxy
import GHC.TypeLits

-- fn1 ------------------------------------------------------------------

class Fn1 (a :: [Nat]) where
    fn1 :: Proxy a -> Integer

instance Fn1 '[] where
    fn1 Proxy = 0

instance (KnownNat p, Fn1 q) => Fn1 ('(:) p q) where
    fn1 Proxy = natVal (Proxy :: Proxy p) + fn1 (Proxy :: Proxy q)

res1 = fn1 (Proxy :: Proxy '[2,3,5])


-- fn2 ----------------------------------------------------------------------

class Fn2 (a :: [Nat]) where
    type Fn2Result a :: [Nat]
    fn2 :: Proxy a -> Proxy (Fn2Result a)

instance Fn2 '[] where
    type Fn2Result '[] = '[]
    fn2 _ = Proxy

instance Fn2 q => Fn2 (p ': q) where
    type Fn2Result (p ': q) = (p+1) ': (Fn2Result q)
    fn2 _ = Proxy

res2 = fn2 (Proxy :: Proxy '[2,3,5])


-- fn3 ----------------------------------------------------------------------
-- I had to use undecidable instances for this...

class Fn3 (a :: [Nat]) where
    type Fn3Result a :: Nat
    fn3 :: Proxy a -> Proxy (Fn3Result a)

instance Fn3 '[] where
    type Fn3Result '[] = 0
    fn3 _ = Proxy

instance Fn3 q => Fn3 (p ': q) where
    type Fn3Result (p ': q) = p + (Fn3Result q)
    fn3 _ = Proxy

res3 = fn3 (Proxy :: Proxy '[2,3,5])


-- fn4 ----------------------------------------------------------------------
-- I'm not quite sure I understand what we're going for here
-- this is the same as Fn3, but without the typeclass?

type family Fn4 (a :: [Nat]) :: Nat
type instance Fn4 '[] = 0
type instance Fn4 (p ': q) = p + (Fn4 q)

res4 = (Proxy :: Proxy (Fn4 '[2,3,5]))