HList.hs

{-|
Module      : Data.HList
Description :
Implementation of strongly typed heterogeneous lists.
Copyright   : (c) Juan García Garland, 2018,2023
License     : GPL
Maintainer  : jpgarcia@fing.edu.uy
Stability   : experimental
Portability : POSIX
|-}

{-# OPTIONS_GHC -fno-warn-missing-methods,
                -fno-warn-partial-type-signatures #-}

{-# LANGUAGE DataKinds,
             TypeOperators,
             PolyKinds,
             GADTs,
             TypeInType,
             RankNTypes,
             StandaloneDeriving,
             FlexibleInstances,
             FlexibleContexts,
             ConstraintKinds,
             MultiParamTypeClasses,
             FunctionalDependencies,
             UndecidableInstances,
             ScopedTypeVariables,
             TypeFamilies,
             InstanceSigs,
             AllowAmbiguousTypes,
             TypeApplications,
             PatternSynonyms,
             PartialTypeSignatures
#-}

module Data.HList where

import Data.Kind
import Data.Proxy
import Data.Label
import Data.Type.Bool
import Data.Type.Equality

-- |Heterogeneous lists are implemented as a GADT
data HList (l :: [Type]) :: Type  where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)

hHead :: HList (t ': _) -> t
hHead (HCons v _) = v


-- | HMember is a test membership function.
--Since we are in Haskell the value level function computes with the evidence 
class HMember (t :: Type) (l :: [Type]) where
  type HMemberRes t l :: Bool
  hMember :: Label t -> HList l -> Proxy (HMemberRes t l)

instance HMember t '[] where
  type HMemberRes t '[] = 'False
  hMember _ _ = Proxy

instance HMember t (t' ': ts) where
  type HMemberRes t (t' ': ts) = t == t' || HMemberRes t ts
  hMember _ _ = Proxy

-- | HMember' is a test membership function.
-- But looking up in a list of Labels
class HMember' (t :: k) (l :: [k]) where
  type HMemberRes' t l :: Bool
  hMember' :: f t -> LList l -> Proxy (HMemberRes' t l)

instance HMember' t '[] where
  type HMemberRes' t '[] = 'False
  hMember' _ _ = Proxy

instance HMember' t (t' ': ts) where
  type HMemberRes' t (t' ': ts) = t == t' || HMemberRes' t ts
  hMember' _ _ = Proxy


-- | No other functionality is needed for AAG

infixr 2 .:
(.:) = HCons
ε = HNil
hn = HNil

-- | a polykinded heteogeneous list of labels
data LList (l :: [k]) :: Type where
  LNil :: LList '[]
  LCons :: Label h -> LList l -> LList (h ': l)

infixr 2 .:.
(.:.) = LCons
lL = LNil

lHead :: LList (t ': ts) -> Label t
lHead _ = Label

class LListFrom (l :: [k]) where
  lListFrom :: Proxy l -> LList l

instance LListFrom ('[] :: [k]) where
  lListFrom (Proxy :: Proxy '[])= LNil

instance LListFrom ts => LListFrom (t ': ts) where
  lListFrom (Proxy :: Proxy (t ': ts))
    = LCons Label $ lListFrom Proxy

type family Snoc (l :: [k]) (v :: k) where
  Snoc '[]       v  = '[v]
  Snoc (x ': xs) v  = x ': Snoc xs v