LevityExperiments.hs

{-# LANGUAGE UnliftedDatatypes, GADTs #-}
module Main where

import Data.Kind
import GHC.Exts

-- type List :: forall {l} . TYPE (BoxedRep l) -> TYPE (BoxedRep l)
--type List :: TYPE (BoxedRep Unlifted) -> TYPE (BoxedRep Unlifted)
data List a :: TYPE (BoxedRep l) where
    Nil :: List a
    Cons :: (a :: TYPE (BoxedRep Unlifted)) -> List a -> List a

-- foldl_ :: forall (a :: TYPE (BoxedRep Unlifted)) (b :: TYPE (BoxedRep Unlifted)) . (b -> a -
> b) -> b -> List a -> b
foldl_ :: forall (a :: TYPE (BoxedRep Unlifted)) (b :: TYPE (BoxedRep Unlifted)) . (b -> a -> b
) -> b -> List a -> b
foldl_ step acc xs = case xs of
    Nil -> acc
    Cons x xs -> foldl_ step (step acc x) xs

-- I'm having trouble with levity-polymorphism
-- idPolyL :: forall {l :: Levity} (a :: TYPE (BoxedRep l)) . a  -> a
-- idPolyL x = x

main :: IO ()
main = pure ()