CompileTimes.hs

{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}

module CompileTime where

import GHC.TypeLits
import Data.Proxy

type family IsLastZero (xs :: [Nat]) :: Bool where
  IsLastZero '[] = False
  IsLastZero '[0] = True
  IsLastZero (_:xs) = IsLastZero xs

type family FromNatDown (n :: Nat) :: [Nat] where
  FromNatDown 0 = '[0]
  FromNatDown n = n : FromNatDown (n - 1)

class LastZero xs

instance IsLastZero xs ~ True => LastZero xs

type LastZero' xs = IsLastZero xs ~ True

{-

GHCi:

*CompileTime> import Data.Proxy
*CompileTime Data.Proxy>
*CompileTime Data.Proxy> :set -XDataKinds -XGADTs -XFlexibleContexts
*CompileTime Data.Proxy> :set -freduction-depth=0
*CompileTime Data.Proxy> :set +s

*CompileTime Data.Proxy> Proxy :: LastZero (FromNatDown 1000) => Proxy ()
Proxy
(20.17 secs, 86,688 bytes)

*CompileTime Data.Proxy> Proxy :: LastZero' (FromNatDown 1000) => Proxy ()
Proxy
(1.99 secs, 86,688 bytes)

=> type is roughly 10x faster for list size 1000

-}

{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}

module Naturals where

import Data.Type.Bool
import GHC.TypeLits (Nat, Mod)
import Data.Singletons.Prelude
import Data.Singletons.TH

$(genDefunSymbols [''Mod])

type family IsPrime (n :: Nat) :: Bool where
  IsPrime 2 = True
  IsPrime n = Not (Any ((==@#@$$) 0) (Map (ModSym1 n) (EnumFromTo 2 (n - 1))))

class Prime (n :: Nat)

instance IsPrime n ~ True => Prime n

type Prime' n = IsPrime n ~ True

{-

GHCi:

*Naturals> :set -XDataKinds -XGADTs -XFlexibleContexts 
*Naturals> :set -freduction-depth=0
*Naturals> :set +s

*Naturals> Proxy :: Prime 199 => Proxy ()
Proxy
(7.30 secs, 93,192 bytes)

*Naturals> Proxy :: Prime' 199 => Proxy ()
Proxy
(26.34 secs, 93,192 bytes)

=> type is roughly 4x slower

-}