tag:blogger.com,1999:blog-5195188167565410449.post3160846306433363350..comments2015-10-31T08:21:47.984+00:00Comments on Haskell for Maths: Finite fields, part 1DavidAhttp://www.blogger.com/profile/16359932006803389458noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-5195188167565410449.post-57335181571150871262009-09-10T14:28:58.171+01:002009-09-10T14:28:58.171+01:00Hi. I'm pretty new to Haskell programming so a...Hi. I'm pretty new to Haskell programming so all this talk about phantom and dependent types blew me away but it all seems very interested. It just makes me want to delve deeper and deeper into Haskell so thanks alot for that.<br /><br />BTW. I checked out the link that BlackMeph provided http://okmij.org/ftp/ and came across this paper http://okmij.org/ftp/papers/number-parametized-types.pdf by Oleg Kiselyov.<br /><br />If Coq can do it, Haskell can definitely do it so I'm not surprised by the existence of this paper.Dwayne R. Crookshttp://www.blogger.com/profile/08803279692056926645noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-78267841964396486842009-08-23T17:20:04.950+01:002009-08-23T17:20:04.950+01:00@David:
I think the reflection library is a much ...@David:<br /><br />I think the reflection library is a much easier path to go than type level integers.<br /><br />@Sterling:<br /><br />Actually the example of working over a finite field was the original motivating example for the reflection library!<br /><br />In the older version of my monoids library (0.1.36) there was a Ring for modular arithmetic that used reflection.<br /><br />I have not updated it since I factored rings and so forth out of the monoids and rewrote the reflection to carry the reflected term-as-type via a phantom type parameter on a newtype.Edward Kmetthttp://www.blogger.com/profile/16144424873202502715noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-66537380391088134552009-08-20T09:43:23.875+01:002009-08-20T09:43:23.875+01:00Hi all,
Many thanks for the pointers. It sounds l...Hi all,<br /><br />Many thanks for the pointers. It sounds like it is possible to get an approximation to what I want in Haskell, but that it involves somewhat more heavyweight type hackery than I'm really comfortable with.<br /><br />(And for real dependent types in Coq etc, giving up type inference feels like too high a price.)<br /><br />For the moment, the F2, F3, F5 etc types that I defined in the post are sufficient for constructing the combinatorial objects I'm interested in, so I'll leave further investigation of this area to another day.DavidAhttp://www.blogger.com/profile/16359932006803389458noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-24983542613899601352009-08-19T20:57:55.097+01:002009-08-19T20:57:55.097+01:00The reflection package is probably the most standa...The reflection package is probably the most standard way, but you can get 90% there with much less type-hackery, I think. Just encode Fp :: F (Integer -> Integer) -- i.e. everything that was previously a value in a field over a prime now becomes a function *from* a prime to a value in that prime's field. So everything is coded over an arbitrary prime, to be determined later (i.e. passed in once), and you can't mix values from different fields accidentally. I'm not sure this approach has been taken before, but it seems like an elegant win.Sterlinghttp://www.blogger.com/profile/09247125866499343326noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-23882483606855917412009-08-19T07:04:42.814+01:002009-08-19T07:04:42.814+01:00I have a somewhat extensive number theory library,...I have a somewhat extensive number theory library, nothing special, and I've seen several people publish libraries not too dissimilar from my own. So I have given some thought about how to structure a library such as this... however at the time I gave up on doing much with the type system, in the interest of creating something usable more quickly.<br /><br />You have covered two approaches I've considered. If all you care about is finite fields, the latter approach might not be too unreasonable, however I've thought more about how to express modular rings.<br /><br />For the latter case, I've thought about implementing binary numbers in the type system, and use Template Haskell to be able to express types in standard base-10 notation. This should be fairly straightforward, in principle, fo field operations, so long as you can live with the inverse operation being partial. <br /><br />The tricky thing that I anticipate would be implementing type-safe modulus and the chinese remainder theorem. I mean, mod : Z_a -> Z_b is well-defined iff b is a divisor of a, and crt : Z_a * Z_b -> Z_(a*b) needs a and b to be relatively prime. <br /><br />So, if all this was coded up and was finally working, I don't really know how usable it would all be. It would be cute, but could you ultimately compute on moduli that weren't known in advance, for example?<br /><br />Again, the challenge in type systems is more of balancing ease of use with expressivity. ;-)Leon Smithhttp://www.blogger.com/profile/06462854866941248768noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-54474031028615557722009-08-19T06:37:05.571+01:002009-08-19T06:37:05.571+01:00I'm not an expert on dependent types, but yo...I'm not an expert on dependent types, but your intuition is at least somewhat wrong. Dependently typed languages can be compiled, and types can be checked at compile time.<br /><br />The downside is that you lose type inference, and that users will frequently need to provide additional proofs (beyond the lambda terms) if types are to be checked at compile time. <br /><br />However, with things like Coq, you can add proof tactics and decision procedures as part of the library to reduce or eliminate this burden on the user.<br /><br />The trickiest thing about type systems is to balance what can be expressed with ease of use. Hindley-Milner style type systems and many of its extensions offer one particularly sweet spot in this spectrum.Leon Smithhttp://www.blogger.com/profile/06462854866941248768noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-9166046903617844322009-08-19T06:19:38.219+01:002009-08-19T06:19:38.219+01:00I believe that Oleg's method uses MPTCs (for w...I believe that Oleg's method uses MPTCs (for wandering audience: Multi-Parameter Type Classes - functions that pin down the types of its argumnts or result based on other arguments its already been given). You may want to give his site, http://okmij.org/ftp/ a try.BlackMephhttp://www.blogger.com/profile/02745499320156194052noreply@blogger.comtag:blogger.com,1999:blog-5195188167565410449.post-39246282384057030162009-08-19T05:50:13.246+01:002009-08-19T05:50:13.246+01:00Take a look at the prepose pdf, it has a section o...Take a look at the prepose pdf, it has a section on modular arithmatic very similar to what you have done here.<br /><br />http://hackage.haskell.org/package/reflection-0.2.0finlaythttp://www.blogger.com/profile/15396802763658963917noreply@blogger.com