Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Created April 7, 2018 17:21
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save Lysxia/089c0a0ce7900923716cdbf79fc4fa99 to your computer and use it in GitHub Desktop.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeNats
import Prelude hiding (replicate)
data Sing n where
Z :: Sing 0
S :: Sing n -> Sing (1 + n)
data List n a where
Nil :: List 0 a
Cons :: a -> List n a -> List (1 + n) a
deriving instance Show a => Show (List n a)
replicate :: Sing n -> a -> List n a
replicate Z _ = Nil
replicate (S n) a = Cons a (replicate n a)
class SingN n where
singN :: Sing n
instance {-# OVERLAPPING #-} SingN 0 where
singN = Z
instance (n ~ (1 + n'), n' ~ (n - 1), SingN n') => SingN n where
singN = S (singN @n')
main = print (replicate (singN @3) ())
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment