{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Constrained.List where

import Data.Functor.Const
import Data.Kind
import Data.Semigroup (Sum (..))

-- | A heterogeneous list / an inductive tuple.
-- We use this heavily to represent arguments to
-- functions in terms. A term application (c.f. `Constrained.Base`)
-- is represented as `App :: fn as b -> List (Term fn) as -> Term fn b`
-- for example.
data List (f :: k -> Type) (as :: [k]) where
  Nil :: List f '[]
  (:>) :: f a -> List f as -> List f (a : as)

infixr 5 :>

deriving instance (forall a. Show (f a)) => Show (List f as)
deriving instance (forall a. Eq (f a)) => Eq (List f as)

mapList :: (forall a. f a -> g a) -> List f as -> List g as
mapList :: forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall (a :: k). f a -> g a
_ List f as
Nil = forall {k} (f :: k -> *). List f '[]
Nil
mapList forall (a :: k). f a -> g a
f (f a
x :> List f as
xs) = forall (a :: k). f a -> g a
f f a
x forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
:> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall (a :: k). f a -> g a
f List f as
xs

mapListC :: forall c as f g. All c as => (forall a. c a => f a -> g a) -> List f as -> List g as
mapListC :: forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
mapListC forall (a :: k). c a => f a -> g a
_ List f as
Nil = forall {k} (f :: k -> *). List f '[]
Nil
mapListC forall (a :: k). c a => f a -> g a
f (f a
x :> List f as
xs) = forall (a :: k). c a => f a -> g a
f f a
x forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
:> forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
mapListC @c forall (a :: k). c a => f a -> g a
f List f as
xs

mapMList :: Applicative m => (forall a. f a -> m (g a)) -> List f as -> m (List g as)
mapMList :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList forall (a :: k). f a -> m (g a)
_ List f as
Nil = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). List f '[]
Nil
mapMList forall (a :: k). f a -> m (g a)
f (f a
x :> List f as
xs) = forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
(:>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). f a -> m (g a)
f f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList forall (a :: k). f a -> m (g a)
f List f as
xs

mapMListC ::
  forall c as f g m.
  (Applicative m, All c as) =>
  (forall a. c a => f a -> m (g a)) ->
  List f as ->
  m (List g as)
mapMListC :: forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *) (m :: * -> *).
(Applicative m, All c as) =>
(forall (a :: k). c a => f a -> m (g a))
-> List f as -> m (List g as)
mapMListC forall (a :: k). c a => f a -> m (g a)
_ List f as
Nil = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). List f '[]
Nil
mapMListC forall (a :: k). c a => f a -> m (g a)
f (f a
x :> List f as
xs) = forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
(:>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: k). c a => f a -> m (g a)
f f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *) (m :: * -> *).
(Applicative m, All c as) =>
(forall (a :: k). c a => f a -> m (g a))
-> List f as -> m (List g as)
mapMListC @c forall (a :: k). c a => f a -> m (g a)
f List f as
xs

foldMapList :: Monoid b => (forall a. f a -> b) -> List f as -> b
foldMapList :: forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList forall (a :: k). f a -> b
_ List f as
Nil = forall a. Monoid a => a
mempty
foldMapList forall (a :: k). f a -> b
f (f a
a :> List f as
as) = forall (a :: k). f a -> b
f f a
a forall a. Semigroup a => a -> a -> a
<> forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList forall (a :: k). f a -> b
f List f as
as

foldMapListC ::
  forall c as b f. (All c as, Monoid b) => (forall a. c a => f a -> b) -> List f as -> b
foldMapListC :: forall {k} (c :: k -> Constraint) (as :: [k]) b (f :: k -> *).
(All c as, Monoid b) =>
(forall (a :: k). c a => f a -> b) -> List f as -> b
foldMapListC forall (a :: k). c a => f a -> b
_ List f as
Nil = forall a. Monoid a => a
mempty
foldMapListC forall (a :: k). c a => f a -> b
f (f a
a :> List f as
as) = forall (a :: k). c a => f a -> b
f f a
a forall a. Semigroup a => a -> a -> a
<> forall {k} (c :: k -> Constraint) (as :: [k]) b (f :: k -> *).
(All c as, Monoid b) =>
(forall (a :: k). c a => f a -> b) -> List f as -> b
foldMapListC @c forall (a :: k). c a => f a -> b
f List f as
as

appendList :: List f as -> List f bs -> List f (Append as bs)
appendList :: forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList List f as
Nil List f bs
bs = List f bs
bs
appendList (f a
a :> List f as
as) List f bs
bs = f a
a forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
:> forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList List f as
as List f bs
bs

lengthList :: List f as -> Int
lengthList :: forall {k} (f :: k -> *) (as :: [k]). List f as -> Int
lengthList = forall a. Sum a -> a
getSum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Sum a
Sum Int
1)

-- | Append two type-level lists
type family Append as as' where
  Append '[] as' = as'
  Append (a : as) as' = a : Append as as'

-- | Map a type functor over a list
type family MapList (f :: k -> j) as where
  MapList f '[] = '[]
  MapList f (a : as) = f a : MapList f as

-- | A List with a hole in it, can be seen as a zipper
-- over type-level lists.
--
-- We use this to represent contexts over terms in `Constrained.Base`.
-- For example, an application of `f` to a single variable of type `a`
-- would be the pair `(fn as b, ListCtx Value as (HOLE a))` where
-- `HOLE` (c.f. `Constrained.Base`) is isomorphic to `:~:`.
data ListCtx f (as :: [Type]) c where
  (:?) :: c a -> List f as -> ListCtx f (a : as) c
  (:!) :: f a -> ListCtx f as c -> ListCtx f (a : as) c

infixr 5 :?, :!

-- | A Convenient pattern for singleton contexts
pattern NilCtx :: c a -> ListCtx f '[a] c
pattern $bNilCtx :: forall (c :: * -> *) a (f :: * -> *). c a -> ListCtx f '[a] c
$mNilCtx :: forall {r} {c :: * -> *} {a} {f :: * -> *}.
ListCtx f '[a] c -> (c a -> r) -> ((# #) -> r) -> r
NilCtx c = ListCtx Nil c Nil

{-# COMPLETE NilCtx #-}

-- | A view of a `ListCtx` where you see the whole context at the same time.
pattern ListCtx ::
  () => as'' ~ Append as (a : as') => List f as -> c a -> List f as' -> ListCtx f as'' c
pattern $bListCtx :: forall (as'' :: [*]) (f :: * -> *) (c :: * -> *) (as :: [*]) a
       (as' :: [*]).
(as'' ~ Append as (a : as')) =>
List f as -> c a -> List f as' -> ListCtx f as'' c
$mListCtx :: forall {r} {as'' :: [*]} {f :: * -> *} {c :: * -> *}.
ListCtx f as'' c
-> (forall {as :: [*]} {a} {as' :: [*]}.
    (as'' ~ Append as (a : as')) =>
    List f as -> c a -> List f as' -> r)
-> ((# #) -> r)
-> r
ListCtx as c as' <- (toWholeCtx -> ListCtxWhole as c as')
  where
    ListCtx List f as
as c a
c List f as'
as' = forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtxWhole f as c -> ListCtx f as c
fromWholeCtx forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *) (a :: [k]) (c :: k -> *) (as :: k)
       (as' :: [k]).
List f a
-> c as -> List f as' -> ListCtxWhole f (Append a (as : as')) c
ListCtxWhole List f as
as c a
c List f as'
as'

{-# COMPLETE ListCtx #-}

-- | Internals for the `ListCtx` pattern
data ListCtxWhole f as c where
  ListCtxWhole ::
    List f as ->
    c a ->
    List f as' ->
    ListCtxWhole f (Append as (a : as')) c

toWholeCtx :: ListCtx f as c -> ListCtxWhole f as c
toWholeCtx :: forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtx f as c -> ListCtxWhole f as c
toWholeCtx (c a
hole :? List f as
suf) = forall {k} (f :: k -> *) (a :: [k]) (c :: k -> *) (as :: k)
       (as' :: [k]).
List f a
-> c as -> List f as' -> ListCtxWhole f (Append a (as : as')) c
ListCtxWhole forall {k} (f :: k -> *). List f '[]
Nil c a
hole List f as
suf
toWholeCtx (f a
x :! ListCtx f as c
xs)
  | ListCtxWhole List f as
pre c a
hole List f as'
suf <- forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtx f as c -> ListCtxWhole f as c
toWholeCtx ListCtx f as c
xs =
      forall {k} (f :: k -> *) (a :: [k]) (c :: k -> *) (as :: k)
       (as' :: [k]).
List f a
-> c as -> List f as' -> ListCtxWhole f (Append a (as : as')) c
ListCtxWhole (f a
x forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
:> List f as
pre) c a
hole List f as'
suf

fromWholeCtx :: ListCtxWhole f as c -> ListCtx f as c
fromWholeCtx :: forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtxWhole f as c -> ListCtx f as c
fromWholeCtx (ListCtxWhole List f as
Nil c a
hole List f as'
suf) = c a
hole forall (c :: * -> *) a (f :: * -> *) (as :: [*]).
c a -> List f as -> ListCtx f (a : as) c
:? List f as'
suf
fromWholeCtx (ListCtxWhole (f a
x :> List f as
pre) c a
hole List f as'
suf) = f a
x forall (f :: * -> *) a (as :: [*]) (c :: * -> *).
f a -> ListCtx f as c -> ListCtx f (a : as) c
:! forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtxWhole f as c -> ListCtx f as c
fromWholeCtx (forall {k} (f :: k -> *) (a :: [k]) (c :: k -> *) (as :: k)
       (as' :: [k]).
List f a
-> c as -> List f as' -> ListCtxWhole f (Append a (as : as')) c
ListCtxWhole List f as
pre c a
hole List f as'
suf)

fillListCtx :: ListCtx f as c -> (forall a. c a -> f a) -> List f as
fillListCtx :: forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtx f as c -> (forall a. c a -> f a) -> List f as
fillListCtx (ListCtx List f as
pre c a
c List f as'
post) forall a. c a -> f a
f = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList List f as
pre (forall a. c a -> f a
f c a
c forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
:> List f as'
post)

mapListCtx :: (forall a. f a -> g a) -> ListCtx f as c -> ListCtx g as c
mapListCtx :: forall (f :: * -> *) (g :: * -> *) (as :: [*]) (c :: * -> *).
(forall a. f a -> g a) -> ListCtx f as c -> ListCtx g as c
mapListCtx forall a. f a -> g a
nt (ListCtx List f as
pre c a
c List f as'
post) = forall (as'' :: [*]) (f :: * -> *) (c :: * -> *) (as :: [*]) a
       (as' :: [*]).
(as'' ~ Append as (a : as')) =>
List f as -> c a -> List f as' -> ListCtx f as'' c
ListCtx (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall a. f a -> g a
nt List f as
pre) c a
c (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall a. f a -> g a
nt List f as'
post)

mapListCtxC ::
  forall c as f g h. All c as => (forall a. c a => f a -> g a) -> ListCtx f as h -> ListCtx g as h
mapListCtxC :: forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
       (g :: * -> *) (h :: * -> *).
All c as =>
(forall a. c a => f a -> g a) -> ListCtx f as h -> ListCtx g as h
mapListCtxC forall a. c a => f a -> g a
nt (h a
h :? List f as
as) = h a
h forall (c :: * -> *) a (f :: * -> *) (as :: [*]).
c a -> List f as -> ListCtx f (a : as) c
:? forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
mapListC @c forall a. c a => f a -> g a
nt List f as
as
mapListCtxC forall a. c a => f a -> g a
nt (f a
a :! ListCtx f as h
ctx) = forall a. c a => f a -> g a
nt f a
a forall (f :: * -> *) a (as :: [*]) (c :: * -> *).
f a -> ListCtx f as c -> ListCtx f (a : as) c
:! forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
       (g :: * -> *) (h :: * -> *).
All c as =>
(forall a. c a => f a -> g a) -> ListCtx f as h -> ListCtx g as h
mapListCtxC @c forall a. c a => f a -> g a
nt ListCtx f as h
ctx

-- | A function type from `ts` to `res`:
--    FunTy '[Int, Bool] Double = Int -> Bool -> Double
type family FunTy ts res where
  FunTy '[] a = a
  FunTy (a : as) r = a -> FunTy as r

-- | Materialize the shape of the type list `as`, this is very useful
-- for avoiding having to write type classes that recurse over `as`.
listShape :: forall as. TypeList as => List (Const ()) as
listShape :: forall (as :: [*]). TypeList as => List (Const ()) as
listShape = forall (ts :: [*]) (f :: * -> *).
TypeList ts =>
(forall a (as :: [*]). List f as -> f a) -> List f ts
unfoldList (\List (Const ()) as
_ -> forall {k} a (b :: k). a -> Const a b
Const ())

-- | Higher-order functions for working on `List`s
class TypeList ts where
  uncurryList :: FunTy (MapList f ts) r -> List f ts -> r
  uncurryList_ :: (forall a. f a -> a) -> FunTy ts r -> List f ts -> r
  curryList :: (List f ts -> r) -> FunTy (MapList f ts) r
  curryList_ :: (forall a. a -> f a) -> (List f ts -> r) -> FunTy ts r
  unfoldList :: (forall a as. List f as -> f a) -> List f ts

-- | NOTE: the two instances for `TypeList` are `TypeList '[]` and
-- `TypeList '(a : as)`. That way its basically just a structurally
-- recursive function on type-level lists that computes the `TypeList`
-- dictionary.
instance TypeList '[] where
  uncurryList :: forall (f :: * -> *) r. FunTy (MapList f '[]) r -> List f '[] -> r
uncurryList FunTy (MapList f '[]) r
a List f '[]
Nil = FunTy (MapList f '[]) r
a
  uncurryList_ :: forall (f :: * -> *) r.
(forall a. f a -> a) -> FunTy '[] r -> List f '[] -> r
uncurryList_ forall a. f a -> a
_ FunTy '[] r
a List f '[]
Nil = FunTy '[] r
a
  curryList :: forall (f :: * -> *) r.
(List f '[] -> r) -> FunTy (MapList f '[]) r
curryList List f '[] -> r
f = List f '[] -> r
f forall {k} (f :: k -> *). List f '[]
Nil
  curryList_ :: forall (f :: * -> *) r.
(forall a. a -> f a) -> (List f '[] -> r) -> FunTy '[] r
curryList_ forall a. a -> f a
_ List f '[] -> r
f = List f '[] -> r
f forall {k} (f :: k -> *). List f '[]
Nil
  unfoldList :: forall (f :: * -> *).
(forall a (as :: [*]). List f as -> f a) -> List f '[]
unfoldList forall a (as :: [*]). List f as -> f a
_ = forall {k} (f :: k -> *). List f '[]
Nil

instance TypeList as => TypeList (a : as) where
  uncurryList :: forall (f :: * -> *) r.
FunTy (MapList f (a : as)) r -> List f (a : as) -> r
uncurryList FunTy (MapList f (a : as)) r
f (f a
a :> List f as
as) = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
FunTy (MapList f ts) r -> List f ts -> r
uncurryList (FunTy (MapList f (a : as)) r
f f a
a) List f as
as
  uncurryList_ :: forall (f :: * -> *) r.
(forall a. f a -> a) -> FunTy (a : as) r -> List f (a : as) -> r
uncurryList_ forall a. f a -> a
k FunTy (a : as) r
f (f a
a :> List f as
as) = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. f a -> a
k (FunTy (a : as) r
f forall a b. (a -> b) -> a -> b
$ forall a. f a -> a
k f a
a) List f as
as
  curryList :: forall (f :: * -> *) r.
(List f (a : as) -> r) -> FunTy (MapList f (a : as)) r
curryList List f (a : as) -> r
f f a
a = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList (\List f as
xs -> List f (a : as) -> r
f (f a
a forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
:> List f as
xs))
  curryList_ :: forall (f :: * -> *) r.
(forall a. a -> f a) -> (List f (a : as) -> r) -> FunTy (a : as) r
curryList_ forall a. a -> f a
p List f (a : as) -> r
f a
a = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. a -> f a) -> (List f ts -> r) -> FunTy ts r
curryList_ forall a. a -> f a
p (\List f as
xs -> List f (a : as) -> r
f (forall a. a -> f a
p a
a forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
:> List f as
xs))
  unfoldList :: forall (f :: * -> *).
(forall a (as :: [*]). List f as -> f a) -> List f (a : as)
unfoldList forall a (as :: [*]). List f as -> f a
f = let xs :: List f as
xs = forall (ts :: [*]) (f :: * -> *).
TypeList ts =>
(forall a (as :: [*]). List f as -> f a) -> List f ts
unfoldList forall a (as :: [*]). List f as -> f a
f in forall a (as :: [*]). List f as -> f a
f List f as
xs forall {k} (f :: k -> *) (a :: k) (as :: [k]).
f a -> List f as -> List f (a : as)
:> List f as
xs

type family All (c :: k -> Constraint) (as :: [k]) :: Constraint where
  All c '[] = ()
  All c (a : as) = (c a, All c as)