StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POAre type family instance proofs possible?
text
Body
copied!<p>First, I started with some typical type-level natural number stuff.</p> <pre><code>{-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} data Nat = Z | S Nat type family Plus (n :: Nat) (m :: Nat) :: Nat type instance Plus Z m = m type instance Plus (S n) m = S (Plus n m) </code></pre> <p>So I wanted to create a data type representing an n-dimensional grid. (A generalization of what is found at <a href="http://blog.sigfpe.com/2006/12/evaluating-cellular-automata-is.html" rel="noreferrer">Evaluating cellular automata is comonadic</a>.)</p> <pre><code>data U (n :: Nat) x where Point :: x -> U Z x Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x </code></pre> <p>The idea is that the type <code>U num x</code> is the type of a <code>num</code>-dimensional grid of <code>x</code>s, which is "focused" on a particular point in the grid.</p> <p>So I wanted to make this a comonad, and I noticed that there's this potentially useful function I can make:</p> <pre><code>ufold :: (x -> U m r) -> U n x -> U (Plus n m) r ufold f (Point x) = f x ufold f (Dimension ls mid rs) = Dimension (map (ufold f) ls) (ufold f mid) (map (ufold f) rs) </code></pre> <p>We can now implement a "dimension join" that turns an n-dimensional grid of m-dimensional grids into an (n+m)-dimensional grid, in terms of this combinator. This will come in handy when dealing with the result of <code>cojoin</code> which will produce grids of grids.</p> <pre><code>dimJoin :: U n (U m x) -> U (Plus n m) x dimJoin = ufold id </code></pre> <p>So far so good. I also noticed that the <code>Functor</code> instance can be written in terms of <code>ufold</code>.</p> <pre><code>instance Functor (U n) where fmap f = ufold (\x -> Point (f x)) </code></pre> <p>However, this results in a type error.</p> <pre><code>Couldn't match type `n' with `Plus n 'Z' </code></pre> <p>But if we whip up some copy pasta, then the type error goes away.</p> <pre><code>instance Functor (U n) where fmap f (Point x) = Point (f x) fmap f (Dimension ls mid rs) = Dimension (map (fmap f) ls) (fmap f mid) (map (fmap f) rs) </code></pre> <p>Well I hate the taste of copy pasta, so my question is this. <strong>How can I tell the type system that <code>Plus n Z</code> is equal to <code>n</code></strong>? And the catch is this: you can't make a change to the type family instances that would cause <code>dimJoin</code> to produce a similar type error.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload