Ticket #8422: Fancy.hs

File Fancy.hs, 3.5 KB (added by carter, 6 years ago)

fancy type nat fun

Line 
1{-# LANGUAGE PolyKinds   #-}
2{-# LANGUAGE BangPatterns #-}
3{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE TypeFamilies #-}
5{-# LANGUAGE GADTs #-}
6{-# LANGUAGE DeriveDataTypeable #-}
7{-# LANGUAGE TypeOperators #-}
8{-# LANGUAGE FlexibleInstances #-}
9{-# LANGUAGE FlexibleContexts #-}
10{-# LANGUAGE FunctionalDependencies #-}
11{-# LANGUAGE UndecidableInstances #-}
12{-# LANGUAGE ScopedTypeVariables #-}
13--{-# LANGUAGE MultiParamTypeClasses #-}
14
15module Fancy where
16
17import GHC.TypeLits 
18
19import Data.Data
20import Unsafe.Coerce
21
22--- at some point, I should evaluate  using the >= 7.8 type level nats
23--- also this nat type should be perhaps in its own module for sanity reasons
24--data PNat = S !PNat  | Z
25
26
27
28infixr 3 :*
29   
30 
31data Shape (rank :: Nat) where 
32    Nil  :: Shape 0
33    (:*) :: {-# UNPACK #-} !(Int:: *) -> !(Shape r) -> Shape ( 1+ r)
34
35{-|
36index ideas inspired by repa3 / repa4, but
37
38NOTE: for the the low rank cases (eg 1-2 dim arrays)
39should figure out a lighter weight indexing story if that
40winds up being widely used and blocking good fusion. Not doing this For now.
41
42However! Writing high level algorithms in a explicitly pointwise indexing
43heavy way will be a bad bad idea.
44
45-} 
46
47-- using unsafe coerce as a ghetto way of writing the "proof"
48-- this can be made properly type safe if i switch to 7.8 support only
49-- that said
50
51-- reverse an Index Shape tuple   
52reverseShape :: Shape r -> Shape r
53reverseShape Nil = Nil 
54reverseShape shs@(anIx :* rest) = go  shs Nil 
55    where
56        go :: Shape a -> Shape b -> Shape (a+b) -- want r= PSum a b
57        go  Nil res =   res   -- 0 + b = b ==> b=r
58        go (ix :* more )  res =   go more  (ix :* res) --- 1+a + b = r
59
60
61        -- attempt I was making
62        --go :: ((a+b) ~ r, (0+b )~b, (a+0)~a)=> Shape a -> Shape b -> Shape (a+b) -- want r= PSum a b
63        --go  Nil res =   res   -- 0 + b = b ==> b=r
64        --go (ix :* more )  res =   go (more :: Shape (a-1)) ((ix :* res):: Shape (b+1)) --- 1+a + b = r
65
66
67
68--shapePrinciple :: (Shape Z -> Shape tot -> Shape tot)->(Shape (S h))
69
70--type family PSum (a :: PNat) (b :: PNat) :: PNat
71
72--type instance PSum  Z a = a
73--type instance PSum (S a) b = S (PSum a b)
74-- the proper Summation type needs to also have
75--type instance  Psum  a (S b) = S (PSum a b)
76--- but that requires closed type families
77
78
79
80
81
82-- | `Shaped lay sh` is a Shape meant for representing the Array rank and dimensions sh,
83-- with layout lay.
84newtype Shaped lay sh = Shaped sh
85
86-- |  Writing down the common ranks.
87type DIM1 = Shape  1
88type DIM2 = Shape  2 
89type DIM3 = Shape 3 
90
91
92{-
93Fancy.hs:58:35:
94    Could not deduce ((r2 + (1 + b)) ~ (a + b))
95    from the context (r ~ (1 + r1))
96      bound by a pattern with constructor
97                 :* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r),
98               in an equation for ‛reverseShape’
99      at Fancy.hs:54:19-30
100    or from (a ~ (1 + r2))
101      bound by a pattern with constructor
102                 :* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r),
103               in an equation for ‛go’
104      at Fancy.hs:58:13-22
105    NB: ‛+’ is a type function, and may not be injective
106    Expected type: Shape (a + b)
107      Actual type: Shape (r2 + (1 + b))
108    Relevant bindings include
109      res :: Shape b (bound at Fancy.hs:58:27)
110      more :: Shape r2 (bound at Fancy.hs:58:19)
111      go :: Shape a -> Shape b -> Shape (a + b) (bound at Fancy.hs:57:9)
112    In the expression: go more (ix :* res)
113    In an equation for ‛go’: go (ix :* more) res = go more (ix :* res)
114   
115-}