Skip to content

Instantly share code, notes, and snippets.

@acowley
Created Jul 24, 2015
Embed
What would you like to do?
{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures
, MultiParamTypeClasses, PolyKinds, ScopedTypeVariables, TypeFamilies
, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
module GaborTEq where
import GHC.TypeLits (Symbol, symbolVal, KnownSymbol)
import Data.Proxy
data Path (names :: [Symbol]) where
Empty :: Path '[]
Longer :: KnownSymbol name => Proxy name -> Path names -> Path (name ': names)
showPath :: Path ns -> String
showPath Empty = ""
showPath (Longer p Empty) = symbolVal p
showPath (Longer p ps) = symbolVal p ++ " -> " ++ showPath ps
data Nat = Z | S Nat
type family MaybeMap (f :: k -> k') t where
MaybeMap f 'Nothing = 'Nothing
MaybeMap f ('Just a) = 'Just (f a)
type family Index t ts :: Maybe Nat where
Index t '[] = 'Nothing
Index t (t ': ts) = 'Just 'Z
Index t (t' ': ts) = MaybeMap 'S (Index t ts)
type family StripOut i path where
StripOut 'Nothing ns = ns
StripOut ('Just 'Z) (name ': ns) = ns
StripOut ('Just ('S i)) (name ': ns) = name ': StripOut ('Just i) ns
StripOut i '[] = '[]
class StripOutAux (i :: Maybe Nat) ts where
stripOutAux :: proxy i -> Path ts -> Path (StripOut i ts)
instance StripOutAux 'Nothing ts where
stripOutAux _ p = p
instance StripOutAux ('Just 'Z) (t ': ts) where
stripOutAux _ (Longer _ path) = path
instance StripOutAux ('Just i) ts => StripOutAux ('Just ('S i)) (t ': ts) where
stripOutAux _ (Longer n' path) =
Longer n' (stripOutAux (Proxy::Proxy ('Just i)) path)
stripOut :: forall name names i. (i ~ Index name names, StripOutAux i names)
=> Proxy name -> Path names -> Path (StripOut i names)
stripOut _ = stripOutAux (Proxy::Proxy i)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment