Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Jim Apple <jbapple+haskell-cafe <at> gmail.com>
Subject: Re: Developing Programs and Proofs Spontaneously using GADT
Newsgroups: gmane.comp.lang.haskell.cafe
Date: Saturday 4th August 2007 16:11:37 UTC (over 9 years ago)
On 8/4/07, Shin-Cheng Mu  wrote:
> Unfortunately, unlike Omega, Haskell does not provide type
> functions.

Something similar is coming:

http://haskell.org/haskellwiki/GHC/Indexed_types#Instance_declarations_2

> Haskell does not know that Plus m n is actually
> a function and cannot conclude that i=k.
>
> To explicitly state the equality, we assume that there is
> a function plusFn which, given a proof of m + n = i and
> a proof of m + n = k, yields a function converting an i
> in any context to a k. That is:
>
>    plusFn :: Plus m n i -> Plus m n k
>                -> (forall f . f i -> f k)
>

[snip]

> How do I define plusFn? I would like to employ the techniques
> related to equality types [3,4,5], but currently I have not
> yet figured out how.

plusFn :: Plus m n h -> Plus m n k -> f h -> f k
plusFn PlusZ PlusZ x = x
plusFn (PlusS p1) (PlusS p2) x =
    case plusFn p1 p2 Equal of
      Equal -> x

data Equal a b where
    Equal :: Equal a a

Jim
 
CD: 3ms