{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
--{-# LANGUAGE MultiParamTypeClasses #-}
module Fancy where
import GHC.TypeLits
import Data.Data
import Unsafe.Coerce
--- at some point, I should evaluate using the >= 7.8 type level nats
--- also this nat type should be perhaps in its own module for sanity reasons
--data PNat = S !PNat | Z
infixr 3 :*
data Shape (rank :: Nat) where
Nil :: Shape 0
(:*) :: {-# UNPACK #-} !(Int:: *) -> !(Shape r) -> Shape ( 1+ r)
{-|
index ideas inspired by repa3 / repa4, but
NOTE: for the the low rank cases (eg 1-2 dim arrays)
should figure out a lighter weight indexing story if that
winds up being widely used and blocking good fusion. Not doing this For now.
However! Writing high level algorithms in a explicitly pointwise indexing
heavy way will be a bad bad idea.
-}
-- using unsafe coerce as a ghetto way of writing the "proof"
-- this can be made properly type safe if i switch to 7.8 support only
-- that said
-- reverse an Index Shape tuple
reverseShape :: Shape r -> Shape r
reverseShape Nil = Nil
reverseShape shs@(anIx :* rest) = go shs Nil
where
go :: Shape a -> Shape b -> Shape (a+b) -- want r= PSum a b
go Nil res = res -- 0 + b = b ==> b=r
go (ix :* more ) res = go more (ix :* res) --- 1+a + b = r
-- attempt I was making
--go :: ((a+b) ~ r, (0+b )~b, (a+0)~a)=> Shape a -> Shape b -> Shape (a+b) -- want r= PSum a b
--go Nil res = res -- 0 + b = b ==> b=r
--go (ix :* more ) res = go (more :: Shape (a-1)) ((ix :* res):: Shape (b+1)) --- 1+a + b = r
--shapePrinciple :: (Shape Z -> Shape tot -> Shape tot)->(Shape (S h))
--type family PSum (a :: PNat) (b :: PNat) :: PNat
--type instance PSum Z a = a
--type instance PSum (S a) b = S (PSum a b)
-- the proper Summation type needs to also have
--type instance Psum a (S b) = S (PSum a b)
--- but that requires closed type families
-- | `Shaped lay sh` is a Shape meant for representing the Array rank and dimensions sh,
-- with layout lay.
newtype Shaped lay sh = Shaped sh
-- | Writing down the common ranks.
type DIM1 = Shape 1
type DIM2 = Shape 2
type DIM3 = Shape 3
{-
Fancy.hs:58:35:
Could not deduce ((r2 + (1 + b)) ~ (a + b))
from the context (r ~ (1 + r1))
bound by a pattern with constructor
:* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r),
in an equation for ‛reverseShape’
at Fancy.hs:54:19-30
or from (a ~ (1 + r2))
bound by a pattern with constructor
:* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r),
in an equation for ‛go’
at Fancy.hs:58:13-22
NB: ‛+’ is a type function, and may not be injective
Expected type: Shape (a + b)
Actual type: Shape (r2 + (1 + b))
Relevant bindings include
res :: Shape b (bound at Fancy.hs:58:27)
more :: Shape r2 (bound at Fancy.hs:58:19)
go :: Shape a -> Shape b -> Shape (a + b) (bound at Fancy.hs:57:9)
In the expression: go more (ix :* res)
In an equation for ‛go’: go (ix :* more) res = go more (ix :* res)
-}