10-Conventions.purs

module Syntax.TypeLevel.Conventions where

-- This file shows the patterns and naming schemes used when writing
-- type-level programming code. Refer to this whenever you're lost.

-- Entities that have the comment "NANS" mean "no apparent naming scheme".
-- In other words, there is not a naming scheme that people seem to follow.
-- So, name it however you want.

-- Entities that do seem to have naming scheme will have their explanation
-- above them in a comment.

type Value_Level_Type = String

data KindName
foreign import data Value :: KindName

data Proxy :: forall k. k -> Type
data Proxy kind = Proxy

-- NANS
inst :: Proxy Value
inst = Proxy

-- The class name is usually "Is[KindName]"
class IsKindName :: KindName -> Constraint
class IsKindName a where
  -- and the reflect function is usually "reflect[KindName]"
  reflectKindName :: Proxy a -> Value_Level_Type

instance IsKindName Value where
  reflectKindName _ = "value-level value"

-- NANS
class IsKindName a <= ConstrainedToKindName a

-- NANS
instance ConstrainedToKindName Value

-- Usually reify[KindName]
reifyKindName :: forall r
           . Value_Level_Type
          -> (forall a. IsKindName a => Proxy a -> r)
          -> r
reifyKindName _valueLevel function = function inst