Instantly share code, notes, and snippets.

# tsuraan/Fun with TypeLits Created Apr 15, 2014

What would you like to do?
 {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators , ExistentialQuantification #-} import GHC.TypeLits import Data.Proxy data Tree :: * -> Nat -> * where Leaf :: a -> Tree a 0 Node :: Tree a n -> Tree a n -> Tree a (n + 1) instance Show a => Show (Tree a b) where show t = case t of Leaf a -> "Leaf " ++ show a Node l r -> "(" ++ show l ++ ") (" ++ show r ++ ")" instance Show a => Show (SomeTree a) where show (SomeTree t) = "SomeTree " ++ show t append :: Tree a n -> Tree a n -> Tree a (n+1) append = Node depth :: KnownNat n => Tree a n -> Int depth = fromEnum . go Proxy where go :: KnownNat n => Proxy n -> Tree a n -> Integer go p _ = natVal p -- Either these three lines, or the remaining lines must be commented out; -- making both 'depth' and 'dynamically' work in the same program seems tricky. -- data SomeTree a = forall depth. KnownNat depth => SomeTree (Tree a depth) -- depth' :: SomeTree a -> Int -- depth' (SomeTree t) = depth t data SomeTree a = forall depth. SomeTree (Tree a depth) withDepth :: Int -> a -> SomeTree a withDepth 0 n = SomeTree \$ Leaf n withDepth x n = case withDepth (x-1) n of SomeTree x -> SomeTree \$ Node x x dynamically :: IO (SomeTree String) dynamically = do depth <- readLn return \$ withDepth depth "hi"
to join this conversation on GitHub. Already have an account? Sign in to comment