[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
