singleraeh 0.2.0 → 0.2.1

raw patch · 3 files changed

+20/−1 lines, 3 files

Files

CHANGELOG.md +3/−0
singleraeh.cabal +1/−1
src/Singleraeh/List.hs +16/−0

CHANGELOG.md view

@@ -1,3 +1,6 @@+## 0.2.1 (2024-05-27)+* add `Reverse` for lists+ ## 0.2.0 (2024-05-25) * add more singled `Natural` operations * add `Sing` for automatic singling

singleraeh.cabal view

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           singleraeh-version:        0.2.0+version:        0.2.1 synopsis:       raehik's singletons description:    Please see README.md. category:       Types, Data

src/Singleraeh/List.hs view

@@ -1,3 +1,5 @@+{-# LANGUAGE UndecidableInstances #-}+ module Singleraeh.List where  import Data.Kind ( Type )@@ -21,3 +23,17 @@ instance Demotable sa => Demotable (SList sa) where     type Demote (SList sa) = [Demote sa]     demote = demoteSList demote++-- | Reverse a type level list.+type Reverse as = Reverse' '[] as+type family Reverse' (acc :: [k]) (as :: [k]) :: [k] where+  Reverse' acc (a : as) = Reverse' (a : acc) as+  Reverse' acc '[]      = acc++sReverse :: SList sa as -> SList sa (Reverse as)+sReverse as = sReverse' SNil as++sReverse' :: SList sa acc -> SList sa as -> SList sa (Reverse' acc as)+sReverse' acc = \case+  SCons a as -> sReverse' (SCons a acc) as+  SNil       -> acc