Skip to content

@tsuraan /Fun with TypeLits
Created

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
{-# 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"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.