{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# 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 :: PNat) where
Nil :: Shape Z
(:*) :: {-# UNPACK #-} !(Int:: *) -> !(Shape r) -> Shape ( S 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 (PSum 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
-- go (ix :* more ) res = unsafeCoerce $ go more (ix :* res)
-- 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 where
PSum 'Z b = b
PSum a 'Z = a
PSum a ('S b) = 'S (PSum a b)
PSum ('S a) b = 'S (PSum a b)
--PSum 'Z 'Z = 'Z
--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:55:35:
Could not deduce (r1 ~ PSum r1 'Z)
from the context (r ~ 'S r1)
bound by a pattern with constructor
:* :: forall (r :: PNat). Int -> Shape r -> Shape ('S r),
in an equation for ‛reverseShape’
at Fancy.hs:55:19-30
‛r1’ is a rigid type variable bound by
a pattern with constructor
:* :: forall (r :: PNat). Int -> Shape r -> Shape ('S r),
in an equation for ‛reverseShape’
at Fancy.hs:55:19-30
Expected type: Shape r
Actual type: Shape (PSum r 'Z)
Relevant bindings include
rest :: Shape r1 (bound at Fancy.hs:55:27)
In the expression: go shs Nil
In an equation for ‛reverseShape’:
reverseShape shs@(anIx :* rest)
= go shs Nil
where
go :: Shape a -> Shape b -> Shape (PSum a b)
go Nil res = res
go (ix :* more) res = go more (ix :* res)
Fancy.hs:58:25:
Could not deduce (b ~ PSum 'Z b)
from the context (r ~ 'S r1)
bound by a pattern with constructor
:* :: forall (r :: PNat). Int -> Shape r -> Shape ('S r),
in an equation for ‛reverseShape’
at Fancy.hs:55:19-30
or from (a ~ 'Z)
bound by a pattern with constructor
Nil :: Shape 'Z,
in an equation for ‛go’
at Fancy.hs:58:13-15
‛b’ is a rigid type variable bound by
the type signature for go :: Shape a -> Shape b -> Shape (PSum a b)
at Fancy.hs:57:16
Expected type: Shape (PSum a b)
Actual type: Shape b
Relevant bindings include
res :: Shape b (bound at Fancy.hs:58:17)
go :: Shape a -> Shape b -> Shape (PSum a b)
(bound at Fancy.hs:58:9)
In the expression: res
In an equation for ‛go’: go Nil res = res
Fancy.hs:59:35:
Could not deduce (PSum ('S r2) b ~ 'S (PSum r2 b))
from the context (r ~ 'S r1)
bound by a pattern with constructor
:* :: forall (r :: PNat). Int -> Shape r -> Shape ('S r),
in an equation for ‛reverseShape’
at Fancy.hs:55:19-30
or from (a ~ 'S r2)
bound by a pattern with constructor
:* :: forall (r :: PNat). Int -> Shape r -> Shape ('S r),
in an equation for ‛go’
at Fancy.hs:59:13-22
Expected type: Shape (PSum a b)
Actual type: Shape (PSum r2 ('S b))
Relevant bindings include
res :: Shape b (bound at Fancy.hs:59:27)
more :: Shape r2 (bound at Fancy.hs:59:19)
go :: Shape a -> Shape b -> Shape (PSum a b)
(bound at Fancy.hs:58:9)
In the expression: go more (ix :* res)
In an equation for ‛go’: go (ix :* more) res = go more (ix :* res)
-}