[Haskell] De-typechecker: converting from a type to a term
This message presents polymorphic functions that derive a term for a given type -- for a class of fully polymorphic functions: proper and improper combinators. This is better understood on an example: rtest4 f g = rr (undefined::(b -> c) -> (a -> b) -> a -> c) HNil f g *HC> rtest4 (:[]) Just 'x' [Just 'x'] *HC> rtest4 Just Right True Just (Right True) We ask the Haskell typechecker to derive us a function of the specified type. We get the real function, which we can then apply to various arguments. The return result does behave like a `composition' -- which is what the type specifies. Informally, we converted from `undefined' to defined. It must be emphasized that no modifications to the Haskell compiler are needed, and no external programs are relied upon. In particular, however surprising it may seem, we get by without `eval' -- because Haskell has reflexive facilities already built-in. This message contains the complete code. It can be loaded as it is into GHCi -- tested on GHCi 6.2.1 or GHCi snapshot 6.3.20041106. It may take a moment or two to load though. Commenting our tests speeds up the loading. This message presents two different converters from a type to a term. Both derive a program, a term, from its specification, a type -- for a class of fully polymorphic functions. The first converter has just been demonstrated. It is quite limited in that the derived function must be used `polymorphically' -- distinct type variables must be instantiated to different types (or, the user should first instantiate their types and then derive the term). The second converter is far more useful: it can let us `visualize' what a function with a particular type may be doing. For example, it might not be immediately clear what the function of the type (((a -> b -> c) -> (a -> b) -> a -> c) -> (t3 -> t1 -> t2 -> t3) -> t) -> t) is. The test (which is further down) says test9 = reify (undefined::(((a -> b -> c) -> (a -> b) -> a -> c) -> (t3 -> t1 -> t2 -> t3) -> t) -> t) gamma0 *HC> test9 \y -> y (\d h p -> d p (h p)) (\d h p -> d) that is, the function in question is one of the X combinators. It is an improper combinator. A particular application is converting a point-free function into the pointful form to really understand the former. For example, it might take time to comprehend the following expression pz = (((. head . uncurry zip . splitAt 1 . repeat) . uncurry) .) . (.) . flip It is derived by Stephan Hohe in http://www.haskell.org/pipermail/haskell-cafe/2005-February/009146.html Our system says test_pz = reify (undefined `asTypeOf` pz) gamma0 *HC> test_pz \h p y -> h y (p y) So, pz is just the S combinator. As an example below shows, an attempt to derive a term for a type a->b expectedly fails. The type error message essentially says that a |- b is underivable. Our system solves type habitation for a class of functions with polymorphic types. From another point of view, the system is a prover in the implication fragment of intuitionistic logic. Essentially we turn a _type_ into a logical program -- a set of Horn clauses -- which we then solve by SLD resolution. It is gratifying to see that Haskell typeclasses are up to that task. The examples above exhibit fully polymorphic types -- those with *uninstantiated* -- implicitly universally quantified -- type variables. That is, our typeclasses can reify not only types but also type schemas. The ability to operate on and compare *unground* types with *uninstantiated* type variables is often sought but rarely attained. The contribution of this message is the set of primitives for nominal equality comparison and deconstruction of unground types. Earlier these tools were used to implement nested monadic regions in the type-safe manner without imposing the total order on the regions. The monadic regions are described in the paper by M. Fluet and G. Morrisett, ICFP04. The rest of this message is as follows: - equality predicate of type schemas - function types as logic programs. Solving type habitation by SLD resolution - more examples - code -- class Resolve: SLD resolution * Equality predicate of type schemas This is a short remark on the equality predicate of type schemas. In more detail, this topic will be described elsewhere. To obtain the equality, we need the following overlapping instances extensions > {-# OPTIONS -fglasgow-exts #-} > {-# OPTIONS -fallow-undecidable-instances #-} > {-# OPTIONS -fallow-overlapping-instances #-} > {-# OPTIONS -fallow-incoherent-instances #-} > > module HC where We must remark that -fallow-overlapping-instances and -fallow-incoherent-instances extensions are used *exclusively* for the type equality testing. With these extensions and the following declarations class C a where op:: a -> Int instance C a where ... instance C Bool where ... data W = forall a. W a the expr
Re: [Haskell] Re: Type of y f = f . f
On Mon, Feb 28, 2005 at 11:10:40PM -0500, Jim Apple wrote: > Jon Fairbairn wrote: > >If you allow quantification over higher > >kinds, you can do something like this: > > > > d f = f . f > > > > d:: âa::*, b::*â*.(b a â a) â b (b a)â a > > > > What's the problem with > > d :: (forall c . b c -> c) -> b (b a) -> a > d f = f . f > > to which ghci gives the type > > d :: forall a b. (forall c. b c -> c) -> b (b a) -> a Or one could do its dual (?). > d :: (forall c . c -> b c) -> a -> b (b a) > d f = f . f rank-n polymorphism is fun :) now, I guess the tricky thing is creating a function which will work as d head and d (:[]) ... John -- John Meacham - ârepetae.netâjohnâ ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] First Issue of The Monad.Reader is online.
The first issue of The Monad.Reader is available: http://www.haskell.org/hawiki/TheMonadReader_2fIssueOne We'd like to hear what you think: http://www.haskell.org/hawiki/TheMonadReader_2fIssueOne_2fFeedBack -- Shae Matijs Erisson - http://www.ScannedInAvian.com/ - Sockmonster once said: You could switch out the unicycles for badgers, and the game would be the same. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
RE: [Haskell] Re: Type of y f = f . f
It is really too bad the 'middle' version does not work, ie John Fairbarn's version > d1 :: (forall c . b c -> c) -> b (b a) -> a > d1 f = f . f John Meacham's version (dual (?)) > d2 :: (forall c . c -> b c) -> a -> b (b a) > d2 f = f . f Or something in the middle > d3 :: forall e a b . (forall c . e c -> b c) -> (e a) -> (b a) > d3 f = f . f but ghci -fglasgow-exts does not like it :-( Jacques ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] (no subject)
Gtk2Hs - A Haskell GUI library based on the Gtk+ GUI Toolkit. Version 0.9.7.1 is now available from: http://gtk2hs.sourceforge.net/ This release is only needed for Windows users. If you have version 0.9.7 working there is no need to upgrade. Source and binary packages are available for Windows. There are binary packages for Gtk+ 2.4.x and 2.6.x. The binary packages require GHC 6.2.2. You may wish to use Gtk+ 2.6 since it follows the Windows native look and themes whereas Gtk+ 2.4 did not. Installation on Windows is fairly straightforward. There is an installer for Gtk+ on Windows and installing Gtk2Hs just involves unzipping and running a batch file. Instructions are here: http://gtk2hs.sourceforge.net/archives/2005/02/17/installing-on-windows/ For future Gtk2Hs releases we hope to provide an MSI installer to make it even easier. Changes since 0.9.7: * build fixes for Windows * almost all modules now carry LGPL 2.1 license * a couple of extra functions are now bound Other changes and news since the last release announcement: * there is an introductory article by Kenneth Hoste in the first issue of The Monad.Reader: http://www.haskell.org/hawiki/TheMonadReader_2fIssueOne * a complete website redesign * many new screenshots: http://sourceforge.net/project/screenshots.php?group_id=49207 * packages of version 0.9.7 are available for Gentoo and FreeBSD Please report all problems to [EMAIL PROTECTED] . Contributions and feedback are also most welcome. Duncan ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Type of y f = f . f
Actually none of these seem to work: >{-# OPTIONS -fglasgow-exts #-} > >module Main where > >main :: IO () >main = putStrLn "OK" > >d :: (forall c . b c -> c) -> b (b a) -> a >d f = f . f > >t0 = d id >t1 = d head >t2 = d fst Load this into GHCI and you get: Test.hs:11:7: Couldn't match the rigid variable `c' against `b c' `c' is bound by the polymorphic type `forall c. b c -> c' at Test.hs:11:5-8 Expected type: b c -> c Inferred type: b c -> b c In the first argument of `d', namely `id' In the definition of `t0': t0 = d id Test.hs:13:5: Inferred type is less polymorphic than expected Quantified type variable `c' escapes It is mentioned in the environment: t2 :: (c, (c, a)) -> a (bound at Test.hs:13:0) In the first argument of `d', namely `fst' In the definition of `t2': t2 = d fst Failed, modules loaded: none. Keean. Jacques Carette wrote: It is really too bad the 'middle' version does not work, ie John Fairbarn's version d1 :: (forall c . b c -> c) -> b (b a) -> a d1 f = f . f John Meacham's version (dual (?)) d2 :: (forall c . c -> b c) -> a -> b (b a) d2 f = f . f Or something in the middle d3 :: forall e a b . (forall c . e c -> b c) -> (e a) -> (b a) d3 f = f . f but ghci -fglasgow-exts does not like it :-( Jacques ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Type of y f = f . f
Here's a type that fits: d :: forall b a t c. (F t c b, F t a c) => t -> a -> b from the following code: >-# OPTIONS -fglasgow-exts #-} >module Main where > >main :: IO () >main = putStrLn "OK" > >data ID = ID >data HEAD = HEAD >data FST = FST > >class F t a b | t a -> b where >f :: t -> a -> b >instance F ID a a where >f _ a = a >instance F HEAD [a] a where >f _ a = head a >instance F FST (a,b) a where >f _ a = fst a > >d :: (F t a c, F t c b) => t -> a -> b >d t = f t . f t > >t0 a = d ID a >t1 a = d HEAD a >t2 a = d FST a Keean. Jim Apple wrote: Is there a type we can give to y f = f . f y id y head y fst are all typeable? Jim Apple ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Type of y f = f . f
On 2005-02-28 at 23:10EST Jim Apple wrote: > Jon Fairbairn wrote: > > If you allow quantification over higher > > kinds, you can do something like this: > > > >d f = f . f > > > >d:: âa::*, b::*â*.(b a â a) â b (b a)â a > > > > What's the problem with > > d :: (forall c . b c -> c) -> b (b a) -> a > d f = f . f > > to which ghci gives the type > > d :: forall a b. (forall c. b c -> c) -> b (b a) -> a It's too restrictive: it requires that the argument to d be polymorphic, so if f:: [Int]->[Int], d f won't typecheck. It also requires that the type of f have an application on the lhs, so f :: Int->Int won't allow d f to typecheck either. In the imaginary typesystem I was thinking of above, we could instantiate b with (Îx.x). As others have pointed out, there are other typesystems that allow different types that also work. Incidentally, I think Ponder would have assigned types to the examples, just not very useful ones; d head would have come out as (Ît.[t])->(Ît.[t]) (assuming anything came out at all). -- JÃn Fairbairn Jon.Fairbairn at cl.cam.ac.uk ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Type of y f = f . f
Jon Fairbairn wrote: If you allow quantification over higher kinds, you can do something like this: d f = f . f d:: âa::*, b::*â*.(b a â a) â b (b a)â a What's the problem with d :: (forall c . b c -> c) -> b (b a) -> a d f = f . f to which ghci gives the type d :: forall a b. (forall c. b c -> c) -> b (b a) -> a It's too restrictive: it requires that the argument to d be polymorphic, so if f:: [Int]->[Int], d f won't typecheck. Oh, that's bad. It also requires that the type of f have an application on the lhs, so f :: Int->Int won't allow d f to typecheck either. This part I don't understand - isn't b anything in *->*? Can't b be the identity functor? Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell