Skip to content

Instantly share code, notes, and snippets.

@banacorn
Created Oct 15, 2015
Embed
What would you like to do?
{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, PolyKinds, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, OverlappingInstances #-}
module Sandbox2 where
import GHC.TypeLits
import Data.Proxy
--------------------------------------------------------------------------------
-- Heterogeneous list
--------------------------------------------------------------------------------
data HList :: [ * ] -> * where
HNil :: HList '[]
HCons :: a -> HList ts -> HList (a ': ts)
-- example
h0 :: HList '[Int, Bool, (), Char]
h0 = HCons 3 (HCons True (HCons () (HCons 'a' HNil)))
--------------------------------------------------------------------------------
-- Nat (type level)
--------------------------------------------------------------------------------
-- type term term
data N = Zero | Suc N
-- example
n3 :: N
n3 = Suc (Suc (Suc Zero))
--------------------------------------------------------------------------------
-- Nat (term level), indexed by type level Nat
--------------------------------------------------------------------------------
-- type kind -> kind
data SNat :: N -> * where
SZero :: SNat 'Zero
SSuc :: SNat n -> SNat ('Suc n)
-- example
sn3 :: SNat (Suc (Suc (Suc Zero)))
sn3 = SSuc (SSuc (SSuc SZero))
--------------------------------------------------------------------------------
-- Nth (type level & term level)
--------------------------------------------------------------------------------
type family Nth (n :: N) (xs :: [k]) :: k where
Nth 'Zero (x ': xs) = x
Nth ('Suc n) (x ': xs) = Nth n xs
-- nth : forall xs . (n : Nat) -> (HList xs) -> xs !! n
nth :: SNat n -> HList xs -> Nth n xs
nth SZero (HCons x xs) = x
nth (SSuc n) (HCons x xs) = nth n xs
-- example
nth0 :: Nth 'Zero '[Int, Bool]
nth0 = 3
nth1 :: Char
nth1 = nth sn3 h0 -- => 'a'
--------------------------------------------------------------------------------
-- Symbol list
--------------------------------------------------------------------------------
-- Symbol :: Kind
-- "asdf", "asf", "asdfsf" :: Symbol
-- type
data SymList :: [ Symbol ] -> * where
SymNil :: SymList '[]
SymCons :: Proxy s -> SymList ts -> SymList (s ': ts)
-- data Proxy a = Proxy
-- example
symList0 :: SymList '[]
symList0 = SymNil
symList1 :: SymList '[ "haha" , "hehe", "lol" ]
symList1 = SymCons Proxy (SymCons Proxy (SymCons Proxy SymNil))
--------------------------------------------------------------------------------
-- Find on Symbol List (type level & term level)
--------------------------------------------------------------------------------
type family SFind (s :: Symbol) (xs :: [Symbol]) :: Symbol where
SFind s (s ': xs) = s -- found!
SFind s (x ': xs) = SFind s xs -- keep looking
-- SFind s '[] = "not found" -- ???
sfind :: Proxy s -> SymList xs -> Proxy (SFind s xs)
sfind s xs = Proxy
-- example
-- sfind0 :: Proxy "hehe"
sfind0 :: Proxy (SFind "hehe" '[ "haha" , "hehe", "lol" ])
sfind0 = Proxy -- lame
-- symbolVal :: Proxy s -> String
sfind1 :: String
sfind1 = symbolVal (sfind (Proxy :: Proxy "haha") symList1)
-- sfind1 => "haha"
--------------------------------------------------------------------------------
-- Associtate List
--------------------------------------------------------------------------------
data Dict :: [ (Symbol, *) ] -> * where
DictNil :: Dict '[]
DictCons :: Proxy s -- key
-> x -- value
-> Dict ts -- old dict
-> Dict ('(s, x) ': ts) -- new dict
-- example
dict0 :: Dict '[ '("hahahahah", Char), '("int", Int) ]
dict0 = DictCons (Proxy :: Proxy "hahahahah") 'a' (DictCons (Proxy :: Proxy "int") 3 DictNil)
--------------------------------------------------------------------------------
-- Find on Dict (type level & term level)
--------------------------------------------------------------------------------
type family Find (s :: Symbol) (xs :: [(Symbol, *)]) :: * where
Find s ('(s, x) ': xs) = x -- found!
Find s ('(z, x) ': xs) = Find s xs -- keep searching
class Findable (s :: Symbol) (xs :: [(Symbol, *)]) where
find :: Proxy s -> Dict xs -> Find s xs
instance Findable s ('(s, x) ': xs) where
find s (DictCons s' x xs) = x
instance (Findable s xs) => Findable s ('(z, x) ': xs) where
find s (DictCons s' x xs) = find s xs
-- find s DictNil = undefined
-- -- find s (DictCons s' x xs) = undefined
-- find s (DictCons s' x xs) | s == s' = x
-- | s /= s' = find s xs
-- example
find0 :: Find "bool" '[ '("bool", Bool), '("int", Int) ]
find0 = True
--------------------------------------------------------------------------------
-- Monadish
--------------------------------------------------------------------------------
class Monadish m where
gret :: a -> m p p a
gbind :: m p q a -> (a -> m q r b) -> m p r b
newtype VST m p q a = VST { unVST :: p -> m (a, q) }
instance Monad m => Monadish (VST m) where
gret x = VST (\s -> return (x, s))
(VST m) `gbind` f = VST (\s0 -> do
(a, s1) <- m s0
unVST (f a) s1)
data TypeRep = TypeRep String
deriving (Eq, Show)
-- insert a key-type relation
insert :: Monad m => Proxy s -> TypeRep -> VST m (Dict ts) (Dict ('(s, TypeRep) ': ts)) ()
insert key typ = VST $ \dict -> return ((), DictCons key typ dict)
-- get :: Monad m => Proxy s -> VST m (Dict ts) (Dict ts) (Find s ts)
-- get key = VST $ \dict -> return (find key dict, dict)
--
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment