module Syntax.TypeLevel.DefiningCustomKinds where
----------------------
-- To change the value-level type into a type-level type:
data Value_Level_Type
= Value_Level_Value1
| Value_Level_Value2
----------------------
-- We first define a data type that does not have any data constructors.
-- This indicates that `Type_Level_Type` is a kind we created.
data Type_Level_Type
-- Then, we use FFI-like syntax to declare the type-level values that kind
-- has. We do not declare a right hand side (RHS) since it has no values
-- |--------- RHS -------|
-- data SomeType = Value1 | Value2
-- Rather, we indicate that the type is a member of that kind using
-- the following syntax:
foreign import data Type_Level_Value1 :: Type_Level_Type
foreign import data Type_Level_Value2 :: Type_Level_Type
-- Note: there is no corresponding javascript file for this one
-- despite the "foreign import" syntax!
----------------------
-- Using a Boolean-like value-level type as an example...
data YesNo = Yes | No
data YesNoKind
foreign import data YesK :: YesNoKind
foreign import data NoK :: YesNoKind
----------------------