Fwd: Type checking expressions

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

Fwd: Type checking expressions

Peter Podlovics
Hello everyone,

I would like to ask for some advice regarding the type checker part of GHC.
My goal is to determine the type of every expression, pattern etc. in the
syntax tree. Currently the compiler doesn't store this information, so I have
to type check manually. One important aspect is that the program may be ill-typed,
but I still want to extract as much information as possible.

I tried using local type checking functions (eg.: tcInferSigma), but whenever
I used it on an expression that had some "out-of-scope" names in it, it failed.

> f xs = length xs

The reason was that xs was not in the local environment.

My question is: how could I provide the necessary local environment for these
type checking functions? Also in the general case, is it possible to somehow
annotate each expression with its type during the type checking?

The motivation for this is that I want to implement a tool that automatically
corrects ill-typed programs based heuristics. For that I need to know the types
of certain AST nodes.

Peter Podlovics



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Type checking expressions

GHC - devs mailing list

Peter

 

My goal is to determine the type of every expression, pattern etc. in the
syntax tree

 

After type checking is complete, the syntax tree is liberally annotated with types.

 

We do not yet have a function

            hsExprType :: HsExpr Id -> Type

but we do have

            TcHsTyn.hsPatType :: Pat GhcTc -> Type

and you or someone could readily make an equivalent for HsExpr.

 

Most type errors are reported by adding an error constraint, but still returning an annotated tree.

Some, I’m afraid, are still done in the old way, by throwing an exception – so you don’t get back an annotated tree in that case.  But they are relatively rare.

 

Others must have wanted something like this…

 

Simon

 

From: ghc-devs [mailto:[hidden email]] On Behalf Of Peter Podlovics
Sent: 02 March 2018 12:05
To: [hidden email]
Subject: Fwd: Type checking expressions

 

Hello everyone,

I would like to ask for some advice regarding the type checker part of GHC.
My goal is to determine the type of every expression, pattern etc. in the
syntax tree. Currently the compiler doesn't store this information, so I have
to type check manually. One important aspect is that the program may be ill-typed,
but I still want to extract as much information as possible.

I tried using local type checking functions (eg.: tcInferSigma), but whenever
I used it on an expression that had some "out-of-scope" names in it, it failed.

> f xs = length xs

The reason was that xs was not in the local environment.

My question is: how could I provide the necessary local environment for these
type checking functions? Also in the general case, is it possible to somehow
annotate each expression with its type during the type checking?

The motivation for this is that I want to implement a tool that automatically
corrects ill-typed programs based heuristics. For that I need to know the types
of certain AST nodes.

Peter Podlovics

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Type checking expressions

GHC - devs mailing list

Always cc ghc-devs!   Bottle-necking on me may well yield a slow response!   Or even Haskell-café.

 

What is the type of (\x -> [x,y])?   Where y is in scope with type y::a.   Presumably something like   a -> [a]?  Or is it forall a. a -> [a]?  And would your answer change if you had just (\x -> [x,x])?

 

Generalisation is tricky, and for terms with non-closed types it is hard to know what you need in your use-case.  A type like ‘a’ might be a very fine answer!

 

A lot depends on precisely what you are trying to do.

 

Simon

 

From: Peter Podlovics [mailto:[hidden email]]
Sent: 05 March 2018 14:54
To: Simon Peyton Jones <[hidden email]>
Subject: Re: Type checking expressions

 

My main concern with that approach is that it might not give the correct type. For example the hsPatType function only gives unconstrained types, so it is incorrect for any numeric literal, since it gives "a" instead of "Num a => a".

So the question is whether it is possible to retrieve the context of the type variables as well. Also this problem may arise in the case of expressions as well, that is why I scrapped that approach and tried to type check the AST with the TcM monad directly, but without any success.

Could you give me any leads on how to solve this problem?

Thanks in advance,

Peter

 

On Mon, Mar 5, 2018 at 9:44 AM, Simon Peyton Jones <[hidden email]> wrote:

Peter

 

My goal is to determine the type of every expression, pattern etc. in the
syntax tree

 

After type checking is complete, the syntax tree is liberally annotated with types.

 

We do not yet have a function

            hsExprType :: HsExpr Id -> Type

but we do have

            TcHsTyn.hsPatType :: Pat GhcTc -> Type

and you or someone could readily make an equivalent for HsExpr.

 

Most type errors are reported by adding an error constraint, but still returning an annotated tree.

Some, I’m afraid, are still done in the old way, by throwing an exception – so you don’t get back an annotated tree in that case.  But they are relatively rare.

 

Others must have wanted something like this…

 

Simon

 

From: ghc-devs [mailto:[hidden email]] On Behalf Of Peter Podlovics
Sent: 02 March 2018 12:05
To: [hidden email]
Subject: Fwd: Type checking expressions

 

Hello everyone,

I would like to ask for some advice regarding the type checker part of GHC.
My goal is to determine the type of every expression, pattern etc. in the
syntax tree. Currently the compiler doesn't store this information, so I have
to type check manually. One important aspect is that the program may be ill-typed,
but I still want to extract as much information as possible.

I tried using local type checking functions (eg.: tcInferSigma), but whenever
I used it on an expression that had some "out-of-scope" names in it, it failed.

> f xs = length xs

The reason was that xs was not in the local environment.

My question is: how could I provide the necessary local environment for these
type checking functions? Also in the general case, is it possible to somehow
annotate each expression with its type during the type checking?

The motivation for this is that I want to implement a tool that automatically
corrects ill-typed programs based heuristics. For that I need to know the types
of certain AST nodes.

Peter Podlovics

 

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Type checking expressions

Robin Palotai
I tried to click around in the GHC 8.2 tree of http://stuff.codereview.me/ghc/#ghc/compiler/typecheck/TcErrors.hs?corpus=ghc-8.2.1-rc2&signature&line=120, but it seems deferring type errors just reports via a different means, and doesn't change the type-checking behavior. But correct me if I'm wrong.

2018-03-05 17:11 GMT+01:00 Simon Peyton Jones via ghc-devs <[hidden email]>:

Always cc ghc-devs!   Bottle-necking on me may well yield a slow response!   Or even Haskell-café.

 

What is the type of (\x -> [x,y])?   Where y is in scope with type y::a.   Presumably something like   a -> [a]?  Or is it forall a. a -> [a]?  And would your answer change if you had just (\x -> [x,x])?

 

Generalisation is tricky, and for terms with non-closed types it is hard to know what you need in your use-case.  A type like ‘a’ might be a very fine answer!

 

A lot depends on precisely what you are trying to do.

 

Simon

 

From: Peter Podlovics [mailto:[hidden email]]
Sent: 05 March 2018 14:54
To: Simon Peyton Jones <[hidden email]>
Subject: Re: Type checking expressions

 

My main concern with that approach is that it might not give the correct type. For example the hsPatType function only gives unconstrained types, so it is incorrect for any numeric literal, since it gives "a" instead of "Num a => a".

So the question is whether it is possible to retrieve the context of the type variables as well. Also this problem may arise in the case of expressions as well, that is why I scrapped that approach and tried to type check the AST with the TcM monad directly, but without any success.

Could you give me any leads on how to solve this problem?

Thanks in advance,

Peter

 

On Mon, Mar 5, 2018 at 9:44 AM, Simon Peyton Jones <[hidden email]> wrote:

Peter

 

My goal is to determine the type of every expression, pattern etc. in the
syntax tree

 

After type checking is complete, the syntax tree is liberally annotated with types.

 

We do not yet have a function

            hsExprType :: HsExpr Id -> Type

but we do have

            TcHsTyn.hsPatType :: Pat GhcTc -> Type

and you or someone could readily make an equivalent for HsExpr.

 

Most type errors are reported by adding an error constraint, but still returning an annotated tree.

Some, I’m afraid, are still done in the old way, by throwing an exception – so you don’t get back an annotated tree in that case.  But they are relatively rare.

 

Others must have wanted something like this…

 

Simon

 

From: ghc-devs [mailto:[hidden email]] On Behalf Of Peter Podlovics
Sent: 02 March 2018 12:05
To: [hidden email]
Subject: Fwd: Type checking expressions

 

Hello everyone,

I would like to ask for some advice regarding the type checker part of GHC.
My goal is to determine the type of every expression, pattern etc. in the
syntax tree. Currently the compiler doesn't store this information, so I have
to type check manually. One important aspect is that the program may be ill-typed,
but I still want to extract as much information as possible.

I tried using local type checking functions (eg.: tcInferSigma), but whenever
I used it on an expression that had some "out-of-scope" names in it, it failed.

> f xs = length xs

The reason was that xs was not in the local environment.

My question is: how could I provide the necessary local environment for these
type checking functions? Also in the general case, is it possible to somehow
annotate each expression with its type during the type checking?

The motivation for this is that I want to implement a tool that automatically
corrects ill-typed programs based heuristics. For that I need to know the types
of certain AST nodes.

Peter Podlovics

 

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Type checking expressions

Peter Podlovics
Simon:

I would like to keep the constraints as much as possible. So if x :: C a => a then [x] :: C a => [a]. Also in the case of patterns if I have f 5 = 5, then the pattern 5 should have type Num a => a, but currently the type is stored without the Num context (using hsPatType). I don't to imitate the complete type checking process, but is there a way to retrieve these context information as well?

Robin:

The current solution uses the feature you mentioned. This is needed in order to extract the incompletely typed AST from the compiler. The tool then would perform some transformations on the syntax tree to correct the type errors, but for that it must be able to type subexpressions as well. The -fdefer-type-errors flag doesn't help to solve this problem, it only enables us to extract the AST.

Any advice on typing expressions using API functions and retrieving context information would help a great deal.

On Mon, Mar 5, 2018 at 5:25 PM, Robin Palotai <[hidden email]> wrote:
I tried to click around in the GHC 8.2 tree of http://stuff.codereview.me/ghc/#ghc/compiler/typecheck/TcErrors.hs?corpus=ghc-8.2.1-rc2&signature&line=120, but it seems deferring type errors just reports via a different means, and doesn't change the type-checking behavior. But correct me if I'm wrong.

2018-03-05 17:11 GMT+01:00 Simon Peyton Jones via ghc-devs <[hidden email]>:

Always cc ghc-devs!   Bottle-necking on me may well yield a slow response!   Or even Haskell-café.

 

What is the type of (\x -> [x,y])?   Where y is in scope with type y::a.   Presumably something like   a -> [a]?  Or is it forall a. a -> [a]?  And would your answer change if you had just (\x -> [x,x])?

 

Generalisation is tricky, and for terms with non-closed types it is hard to know what you need in your use-case.  A type like ‘a’ might be a very fine answer!

 

A lot depends on precisely what you are trying to do.

 

Simon

 

From: Peter Podlovics [mailto:[hidden email]]
Sent: 05 March 2018 14:54
To: Simon Peyton Jones <[hidden email]>
Subject: Re: Type checking expressions

 

My main concern with that approach is that it might not give the correct type. For example the hsPatType function only gives unconstrained types, so it is incorrect for any numeric literal, since it gives "a" instead of "Num a => a".

So the question is whether it is possible to retrieve the context of the type variables as well. Also this problem may arise in the case of expressions as well, that is why I scrapped that approach and tried to type check the AST with the TcM monad directly, but without any success.

Could you give me any leads on how to solve this problem?

Thanks in advance,

Peter

 

On Mon, Mar 5, 2018 at 9:44 AM, Simon Peyton Jones <[hidden email]> wrote:

Peter

 

My goal is to determine the type of every expression, pattern etc. in the
syntax tree

 

After type checking is complete, the syntax tree is liberally annotated with types.

 

We do not yet have a function

            hsExprType :: HsExpr Id -> Type

but we do have

            TcHsTyn.hsPatType :: Pat GhcTc -> Type

and you or someone could readily make an equivalent for HsExpr.

 

Most type errors are reported by adding an error constraint, but still returning an annotated tree.

Some, I’m afraid, are still done in the old way, by throwing an exception – so you don’t get back an annotated tree in that case.  But they are relatively rare.

 

Others must have wanted something like this…

 

Simon

 

From: ghc-devs [mailto:[hidden email]] On Behalf Of Peter Podlovics
Sent: 02 March 2018 12:05
To: [hidden email]
Subject: Fwd: Type checking expressions

 

Hello everyone,

I would like to ask for some advice regarding the type checker part of GHC.
My goal is to determine the type of every expression, pattern etc. in the
syntax tree. Currently the compiler doesn't store this information, so I have
to type check manually. One important aspect is that the program may be ill-typed,
but I still want to extract as much information as possible.

I tried using local type checking functions (eg.: tcInferSigma), but whenever
I used it on an expression that had some "out-of-scope" names in it, it failed.

> f xs = length xs

The reason was that xs was not in the local environment.

My question is: how could I provide the necessary local environment for these
type checking functions? Also in the general case, is it possible to somehow
annotate each expression with its type during the type checking?

The motivation for this is that I want to implement a tool that automatically
corrects ill-typed programs based heuristics. For that I need to know the types
of certain AST nodes.

Peter Podlovics

 

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs




_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs