Home Reading Searching Subscribe Sponsors Statistics Posting Contact Spam Lists Links About Hosting Filtering Features Download Marketing Archives FAQ Blog From: Jim Apple 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 10 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: 5ms