Created

Embed URL

HTTPS clone URL

SSH clone URL

You can clone with HTTPS or SSH.

Download Gist
View Fun with TypeLits
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
{-# 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.