Working out the types

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Working out the types

Patrick LeBoutillier
Hi all,

Today after reading a question on StackOverflow I found myself
"working out the types" for this expression:

map . (:)

Using a pencil and paper (and more time than I has hoped) I was able
to come to the same answer as given
by ghci:

map . (:) :: a -> [[a]] -> [[a]]


Here's my question: Does ghci have a verbose mode or something where
is can show you step by step how the types
are worked out? If not is there a hackage (or any other kind of)
package that can do that?

I've seen long examples worked out by people on this list (namely
Daniel Ficher) and they are easy to follow and help me
a lot, so I was wondering if such a program existed that could do it
automatically.


Thanks,

Patrick









--
=====================
Patrick LeBoutillier
Rosem?re, Qu?bec, Canada


Reply | Threaded
Open this post in threaded view
|

Working out the types

Daniel Fischer
On Tuesday 05 July 2011, 19:55:43, Patrick LeBoutillier wrote:
> Hi all,

> Here's my question: Does ghci have a verbose mode or something where
> is can show you step by step how the types
> are worked out?

No. You can use it to get the types of subexpressions, though, and work
towards the complete expression from that:

Prelude> :t (:)
(:) :: a -> [a] -> [a]
Prelude> :t (. (:))
(. (:)) :: (([a] -> [a]) -> c) -> a -> c
Prelude> :t (map . (:))
(map . (:)) :: a -> [[a]] -> [[a]]

which gives you smaller gaps to fill in.

> If not is there a hackage (or any other kind of)
> package that can do that?

I'm not aware of any, but there might be.

>
> a lot, so I was wondering if such a program existed that could do it
> automatically.

Automatic type checkers do exist (every compiler/interpreter needs one),
but I don't think they have been written with the ability to output not
only the result but also the derivation.

For someone familiar with a particular type checker, it probably wouldn't
be hard to add that feature, but if it's a complicated beast like GHC's
type checker, becoming familiar with it would probably be a big
undertaking.

Writing your own much-reduced (able to parse and typecheck only a very
restricted subset of the language) might be easier, but probably working
from Mark P. Jones' "Typing Haskell in Haskell"
http://web.cecs.pdx.edu/~mpj/thih/
would be better than starting from scratch (it's somewhat oldish, so it
certainly doesn't cope with recent GHC extensions, but for everyday run-of-
the-mill problems, it should be working with only minor modifications).



Reply | Threaded
Open this post in threaded view
|

Working out the types

Patrick LeBoutillier
Daniel,

The paper you recommend seems like very interesting stuff.  I will
definitely look at it closer.


Thanks a lot,

Patrick


On Tue, Jul 5, 2011 at 3:24 PM, Daniel Fischer
<daniel.is.fischer at googlemail.com> wrote:

> On Tuesday 05 July 2011, 19:55:43, Patrick LeBoutillier wrote:
>> Hi all,
>
>> Here's my question: Does ghci have a verbose mode or something where
>> is can show you step by step how the types
>> are worked out?
>
> No. You can use it to get the types of subexpressions, though, and work
> towards the complete expression from that:
>
> Prelude> :t (:)
> (:) :: a -> [a] -> [a]
> Prelude> :t (. (:))
> (. (:)) :: (([a] -> [a]) -> c) -> a -> c
> Prelude> :t (map . (:))
> (map . (:)) :: a -> [[a]] -> [[a]]
>
> which gives you smaller gaps to fill in.
>
>> If not is there a hackage (or any other kind of)
>> package that can do that?
>
> I'm not aware of any, but there might be.
>
>>
>> a lot, so I was wondering if such a program existed that could do it
>> automatically.
>
> Automatic type checkers do exist (every compiler/interpreter needs one),
> but I don't think they have been written with the ability to output not
> only the result but also the derivation.
>
> For someone familiar with a particular type checker, it probably wouldn't
> be hard to add that feature, but if it's a complicated beast like GHC's
> type checker, becoming familiar with it would probably be a big
> undertaking.
>
> Writing your own much-reduced (able to parse and typecheck only a very
> restricted subset of the language) might be easier, but probably working
> from Mark P. Jones' "Typing Haskell in Haskell"
> http://web.cecs.pdx.edu/~mpj/thih/
> would be better than starting from scratch (it's somewhat oldish, so it
> certainly doesn't cope with recent GHC extensions, but for everyday run-of-
> the-mill problems, it should be working with only minor modifications).
>
>



--
=====================
Patrick LeBoutillier
Rosem?re, Qu?bec, Canada


Reply | Threaded
Open this post in threaded view
|

Working out the types

Patrick LeBoutillier
Hi Daniel,

I took the code that accompanies the paper and I'm trying to use it
but I can't figure out how to get started.
I have the following code but it is not giving me the expected result:

import TypingHaskellInHaskell

mapt = "map" :>: Forall [Star, Star]
             ([] :=>
              ((TGen 0 `fn` TGen 1) `fn` TAp tList (TGen 0) `fn` TAp
tList (TGen 1)))

idt = "id" :>: Forall [Star]
             ([] :=>
              (TGen 0 `fn` TGen 0))

exprt = Ap (Const mapt) (Const idt)

test = runTI $ tiExpr initialEnv [] exprt


When I execute the test function above in ghci I get:

([],TVar (Tyvar "v3" Star)).

I was expecting someting like below for the type part:

TAp tList (TGen 0) `fn` TAp tList (TGen 0)


What I want is the library to compute for me the type of "map id".
What is the proper way to achieve this?



Thanks a lot,

Patrick


On Wed, Jul 6, 2011 at 8:19 AM, Patrick LeBoutillier
<patrick.leboutillier at gmail.com> wrote:

> Daniel,
>
> The paper you recommend seems like very interesting stuff. ?I will
> definitely look at it closer.
>
>
> Thanks a lot,
>
> Patrick
>
>
> On Tue, Jul 5, 2011 at 3:24 PM, Daniel Fischer
> <daniel.is.fischer at googlemail.com> wrote:
>> On Tuesday 05 July 2011, 19:55:43, Patrick LeBoutillier wrote:
>>> Hi all,
>>
>>> Here's my question: Does ghci have a verbose mode or something where
>>> is can show you step by step how the types
>>> are worked out?
>>
>> No. You can use it to get the types of subexpressions, though, and work
>> towards the complete expression from that:
>>
>> Prelude> :t (:)
>> (:) :: a -> [a] -> [a]
>> Prelude> :t (. (:))
>> (. (:)) :: (([a] -> [a]) -> c) -> a -> c
>> Prelude> :t (map . (:))
>> (map . (:)) :: a -> [[a]] -> [[a]]
>>
>> which gives you smaller gaps to fill in.
>>
>>> If not is there a hackage (or any other kind of)
>>> package that can do that?
>>
>> I'm not aware of any, but there might be.
>>
>>>
>>> a lot, so I was wondering if such a program existed that could do it
>>> automatically.
>>
>> Automatic type checkers do exist (every compiler/interpreter needs one),
>> but I don't think they have been written with the ability to output not
>> only the result but also the derivation.
>>
>> For someone familiar with a particular type checker, it probably wouldn't
>> be hard to add that feature, but if it's a complicated beast like GHC's
>> type checker, becoming familiar with it would probably be a big
>> undertaking.
>>
>> Writing your own much-reduced (able to parse and typecheck only a very
>> restricted subset of the language) might be easier, but probably working
>> from Mark P. Jones' "Typing Haskell in Haskell"
>> http://web.cecs.pdx.edu/~mpj/thih/
>> would be better than starting from scratch (it's somewhat oldish, so it
>> certainly doesn't cope with recent GHC extensions, but for everyday run-of-
>> the-mill problems, it should be working with only minor modifications).
>>
>>
>
>
>
> --
> =====================
> Patrick LeBoutillier
> Rosem?re, Qu?bec, Canada
>



--
=====================
Patrick LeBoutillier
Rosem?re, Qu?bec, Canada