{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Overloaded.Lists (
Nil (..),
Cons (..),
fromList,
) where
import Data.Coerce (coerce)
import Data.List.NonEmpty (NonEmpty (..))
import Data.SOP.NP (NP (..), POP (..))
import qualified Data.IntSet as IS
import qualified Data.Set as S
import qualified Data.Type.Nat as N
import qualified Data.Vec.Lazy as Vec
class Nil a where
nil :: a
class Cons x ys zs | zs -> x ys where
cons :: x -> ys -> zs
fromList :: (Nil xs, Cons x xs xs) => [x] -> xs
fromList = foldr cons nil
instance Nil [a] where
nil = []
instance Cons a [a] [a] where
cons = (:)
instance Cons a [a] (NonEmpty a) where
cons = (:|)
instance Nil (S.Set a) where
nil = S.empty
instance Ord a => Cons a (S.Set a) (S.Set a) where
cons = S.insert
instance Nil IS.IntSet where
nil = IS.empty
instance Cons Int IS.IntSet IS.IntSet where
cons = IS.insert
instance n ~ 'N.Z => Nil (Vec.Vec n a) where
nil = Vec.VNil
instance Cons a (Vec.Vec n a) (Vec.Vec ('N.S n) a) where
cons = (Vec.:::)
instance xs ~ '[] => Nil (NP f xs) where
nil = Nil
instance Cons (f x) (NP f xs) (NP f (x ': xs)) where
cons = (:*)
instance xs ~ '[] => Nil (POP f xs) where
nil = POP Nil
instance Cons (NP f xs) (POP f xss) (POP f (xs ': xss)) where
cons = coerce (cons :: NP f xs -> NP (NP f) xss -> NP (NP f) (xs ': xss))