#4385: Type-level natural numbers
----------------------------------------+-----------------------------------
Reporter: diatchki | Owner: diatchki
Type: feature request | Status: new
Priority: normal | Milestone: 7.2.1
Component: Compiler (Type checker) | Version:
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by pumpkin):
The main application I'm thinking about is REPA right now, which uses a
fairly complex type to describe the shape of multidimensional arrays. The
type is, however, not fully representative of the actual shape of the
array, because we don't have easy type-level naturals. There's also some
confusing overlap between the type-level shape (which mostly encodes the
number of dimensions of the array) and the value-level shape (which
actually contains the dimensions).
Using your typenats and some fancy GADT trickery, the index computations
could be made exact and proved correct at compile time, to avoid any kind
of index checking at runtime, but the computation is non-trivial, and
basically involves proving that if you have a list of dimensions and a
list of indices, then the usual multidimensional flattening computation
preserves the < length requirement for the flat underlying array. I was
modeling REPA in Agda a while back and came up with this:
{{{
data Shape : ℕ → Set where
Z : Shape 1
_∷_ : ∀ {n} → (ss : Shape n) → (s : ℕ) → Shape (suc s * n)
data Index : ∀ {n} → Shape n → Set where
Z : Index Z
_∷_ : ∀ {m} {sh : Shape m} {n} → (is : Index sh) → (i : Fin (suc n)) →
Index (sh ∷ n)
flatten : ∀ {n} {sh : Shape n} → Index sh → Fin n
flatten = {- lots more stuff to prove that the flattening computation
preseves the Fin -}
}}}
Although this is dependently typed in Agda, it could be modeled in Haskell
too using GADTs that refine the type index to a typenat multiplication.
When I get the time to compile your repo, I'll try translating this to
Haskell with typenats and see if it can spot the fairly complicated
behavior that I need to prove manually in Agda. I'll be very happy if it
can!
Anyway, it's an exciting development in GHC! Now you just have to fight
off all the proof-freaks like me that it attracts :P
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:17>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
