Re: [Haskell-cafe] Type checking the content of a string

Finally, I solved the problem using typeOf instead of interpret: cr :: QuasiQuoter cr = QuasiQuoter { quoteExp = quoteRuleFunc} quoteRuleFunc :: String -> Q TH.Exp quoteRuleFunc s = do res <- runIO $ runInterpreter $ do setImports ["Prelude", "Language.Nomyx.Expression"] typeOf s

Re: [Haskell-cafe] Type checking the content of a string

strings. > However, how could I be sure that these test program are syntactically > valid, at compile time? If you just want to check whether a program is syntactically valid, you can use the haskell-src-exts package to parse it. If you also want to do some type checking you can try th

Re: [Haskell-cafe] Type checking the content of a string

Up on that, anybody already tried to load an haskell interpreter in a QuasiQuoter? On Sat, Feb 23, 2013 at 12:03 AM, Corentin Dupont wrote: > I'm trying to load my interpreter in the Q monad: > > cr :: QuasiQuoter > cr = QuasiQuoter { quoteExp = quoteRuleFunc} > > quoteRuleFunc :: String -> Q TH

Re: [Haskell-cafe] Type checking the content of a string

I'm trying to load my interpreter in the Q monad: cr :: QuasiQuoter cr = QuasiQuoter { quoteExp = quoteRuleFunc} quoteRuleFunc :: String -> Q TH.Exp quoteRuleFunc s = do res <- runIO $ runInterpreter $ do setImports ["Prelude", "Language.Nomyx.Rule", "Language.Nomyx.Expression", "Languag

Re: [Haskell-cafe] Type checking the content of a string

Great! That seems very powerful. So you can do what you want during compilation, readin files, send data over the network? Other question, in my example how can I halt the compilation if a test program is wrong? On Fri, Feb 22, 2013 at 8:30 PM, Francesco Mazzoli wrote: > At Fri, 22 Feb 2013 19:4

Re: [Haskell-cafe] Type checking the content of a string

At Fri, 22 Feb 2013 19:43:51 +0100, Corentin Dupont wrote: > Hi Adam, > that looks interresting. I'm totally new to TH and QuasiQuotes, though. > Can I run IO in a QuasiQuoter? I can run my own interpreter. Yes, you can:

Re: [Haskell-cafe] Type checking the content of a string

Hi Adam, that looks interresting. I'm totally new to TH and QuasiQuotes, though. Can I run IO in a QuasiQuoter? I can run my own interpreter. On Fri, Feb 22, 2013 at 7:12 PM, adam vogt wrote: > On Fri, Feb 22, 2013 at 12:44 PM, Corentin Dupont > wrote: > > Hi all, > > I have a program able to

Re: [Haskell-cafe] Type checking the content of a string

On Fri, Feb 22, 2013 at 12:44 PM, Corentin Dupont wrote: > Hi all, > I have a program able to read another program as a string, and interpret it > (using Hint). > I'd like to make unit tests, so I have a file "Test.hs" containing a serie > of test programs as strings. > However, how could I be sur

[Haskell-cafe] Type checking the content of a string

Hi all, I have a program able to read another program as a string, and interpret it (using Hint). I'd like to make unit tests, so I have a file "Test.hs" containing a serie of test programs as strings. However, how could I be sure that these test program are syntactically valid, at compile time? Th

[Haskell-cafe] Haskell V Java type checking

checking over the Java type checking? 3) Are there more general advantages of Haskell type checking over Java type checking?Regards,Pat Haskell program===data Cdata Dclass A t whereinstance A C whereinstance A D whereclass A t => B t whereinstance B C whereinstance B D where=Java Prog

Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion

t deconstruction but prohibit construction. They are quite handy, saving us trouble writing the views like isAssign. > Actually... to go a bit further, I thought there was some way to arrange > this so that, upon GHC type-checking the case statement, it would realize > that certai

Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion

ually... to go a bit further, I thought there was some way to arrange this so that, upon GHC type-checking the case statement, it would realize that certain cases are forbidden based on the type, and would consider the pattern match complete without them (or issue an error if they are present). T

Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion

On 07/12/2011 05:01 PM, Ryan Newton wrote: Hi all, Is there something wrong with the code below? My anticipation was that the type of "test" would include the class constraint, because it uses the Assign constructor. But if you load this code in GHCI you can see that the inferred type was "tes

Re: [Haskell-cafe] Type checking oddity -- maybe my own confusion

1 16:02 To: Haskell Cafe Subject: [Haskell-cafe] Type checking oddity -- maybe my own confusion Hi all, Is there something wrong with the code below? My anticipation was that the type of "test" would include the class constraint, because it uses the Assign constructor. But if you lo

[Haskell-cafe] Type checking oddity -- maybe my own confusion

Hi all, Is there something wrong with the code below? My anticipation was that the type of "test" would include the class constraint, because it uses the Assign constructor. But if you load this code in GHCI you can see that the inferred type was "test :: E m -> E m". Thanks, -Ryan {-# LANG

Re: [Haskell-cafe] Manual Type-Checking to provide Read instances for GADTs. (was Re: [Haskell-cafe] Read instance for GATD)

That's really nice. Very interesting. Thank you. On Fri, Jun 25, 2010 at 9:55 PM, Edward Kmett wrote: > I've obtained permission to repost Gershom's slides on how to deserialize > GADTs by typechecking them yourself, which are actually a literate haskell > source file, that he was rendering to s

Re: [Haskell-cafe] Manual Type-Checking to provide Read instances for GADTs. (was Re: [Haskell-cafe] Read instance for GATD)

I've obtained permission to repost Gershom's slides on how to deserialize GADTs by typechecking them yourself, which are actually a literate haskell source file, that he was rendering to slides. Consequently, I've just pasted the content below as a literate email. -Edward Kmett - Deserializing st

[Haskell-cafe] Re: Non-termination of type-checking

> And I'm pretty sure that there's no way to convince Agda that F = R, > or something similar, because, despite the fact that Agda has > injective type constructors like GHC (R x = R y => x = y), it doesn't > let you make the inference R Unit = F Unit => R = F. Of course, in > Agda, one could ar

[Haskell-cafe] Re: Non-termination of type-checking

On Saturday 30 January 2010 3:44:35 am o...@okmij.org wrote: > It seems likely `absurd' diverges in GHCi is because of the GHC > inliner. The paper about secrets of the inliner points out that the > aggressiveness of the inliner can cause divergence in the compiler > when processing code with negat

[Haskell-cafe] Re: Non-termination of type-checking

Thanks for the clear explanation, oleg. -- ryan On Sat, Jan 30, 2010 at 12:44 AM, wrote: > > We explain the technique of systematically deriving absurd terms and > apply it to type families. > > Indeed I should have said that there is no _overt_ impredicative > polymorphism in the example pos

[Haskell-cafe] Re: Non-termination of type-checking

We explain the technique of systematically deriving absurd terms and apply it to type families. Indeed I should have said that there is no _overt_ impredicative polymorphism in the example posted earlier: it is precisely the impredicative polymorphism that causes the paradox. As everybody notice

Re: [Haskell-cafe] Re: Non-termination of type-checking

s imminent. > > > > We reach the conclusion that an instance of a non-recursive GADT > > can be a recursive type. GADT may harbor recursion, so to speak. > > > > The code below, when loaded into GHCi 6.10.4, diverges on > > type-checking. It type-checks when we co

Re: [Haskell-cafe] Re: Non-termination of type-checking

On Friday 29 January 2010 5:26:28 pm Matthieu Sozeau wrote: > data R (c :: *) where >R :: forall c' :: * -> *, (c' (c' ()) -> False) -> R (c' ()). This is what the data declaration is. The c on the first line and the c on the second line are unrelated. It's sort of an oddity of GADT declarati

[Haskell-cafe] Re: Non-termination of type-checking

speak. The code below, when loaded into GHCi 6.10.4, diverges on type-checking. It type-checks when we comment-out absurd. {-# LANGUAGE GADTs, EmptyDataDecls #-} data False -- No constructors data R c where -- Not recursive R :: (c (c

Re: [Haskell-cafe] Re: Non-termination of type-checking

pe. GADT may harbor recursion, so to speak. > > The code below, when loaded into GHCi 6.10.4, diverges on > type-checking. It type-checks when we comment-out absurd. > > > {-# LANGUAGE GADTs, EmptyDataDecls #-} > > data False -- No constr

Re: [Haskell-cafe] Re: Non-termination of type-checking

be a recursive type. GADT may harbor recursion, so to speak. > > The code below, when loaded into GHCi 6.10.4, diverges on > type-checking. It type-checks when we comment-out absurd. > > > {-# LANGUAGE GADTs, EmptyDataDecls #-} > > data False

Re: [Haskell-cafe] Non-termination of type-checking

On Thu, 28 Jan 2010 18:32:02 -0800, Ryan Ingram wrote: > But your example uses a recursive type; the interesting bit about this > example is that there is no recursive types or function, and yet we > can encode this loop. The point is that you get the Fix type by (infintely) unfolding the type de

[Haskell-cafe] Re: Non-termination of type-checking

, diverges on type-checking. It type-checks when we comment-out absurd. {-# LANGUAGE GADTs, EmptyDataDecls #-} data False -- No constructors data R c where -- Not recursive R :: (c (c ()) -> False) -> R (c ()) -- instantiate c to R, so

Re: [Haskell-cafe] Non-termination of type-checking

But your example uses a recursive type; the interesting bit about this example is that there is no recursive types or function, and yet we can encode this loop. -- ryan On Wed, Jan 27, 2010 at 4:49 PM, Matthew Brecknell wrote: > Ryan Ingram wrote: >> The compiler doesn't loop for me with GHC6.

Re: [Haskell-cafe] Non-termination of type-checking

Ryan Ingram wrote: > The compiler doesn't loop for me with GHC6.10.4; I think GADTs still > had some bugs in GHC6.8. > > That said, this is pretty scary. Here's a simplified version that > shows this paradox with just a single GADT and no other extensions. > No use of "fix" or recursion anywhere!

Re: [Haskell-cafe] Non-termination of type-checking

; >>                    case eq of -- Uses injectivity of type constructors >>                     Eqrefl -> f ax) > >> r_eqv_not_R_1 :: R (I R) -> R (I R) -> False >> r_eqv_not_R_1 = r_eqv1 > >> r_eqv_not_R_2 :: (R (I R) -> False) -> R (I

[Haskell-cafe] Non-termination of type-checking

eqv1 > r_eqv_not_R_2 :: (R (I R) -> False) -> R (I R) > r_eqv_not_R_2 = r_eqv2 > rir :: R (I R) > rir = r_eqv_not_R_2 (\ rir -> r_eqv_not_R_1 rir rir) Type checking seems to loop here with ghc-6.8.3, which is a bit strange given the simplicity of the typing problem. Maybe it

Re: [Haskell-cafe] Naive booleans and numbers - type-checking fails

lper functions such a way, so that definition in lambda-calculus can be > used in a straightforward way in Haskell. I was caught in trouble quite soon > during change of lambda-expressions to Haskell - defining prefn as a helper > for prev. When using Haskell-ish if-then-else then there is

Re: [Haskell-cafe] Naive booleans and numbers - type-checking fails

On Sun, Jan 24, 2010 at 3:12 PM, Stephen Tetley wrote: > Doesn't the simply typed lambda calculus introduce if-then-else as a > primitive precisely so that it can be typed? > > Its not an illuminating answer to your question and I'd welcome > clarification for my own understanding, but I don't thi

Re: [Haskell-cafe] Naive booleans and numbers - type-checking fails

Doesn't the simply typed lambda calculus introduce if-then-else as a primitive precisely so that it can be typed? Its not an illuminating answer to your question and I'd welcome clarification for my own understanding, but I don't think you can solve the problem without appealing to Haskell's built

[Haskell-cafe] Naive booleans and numbers - type-checking fails

ining prefn as a helper for prev. When using Haskell-ish if-then-else then there is no problem (the code commented out), while using defined if-then-else (mif), the type-checking fails, but just for this case! Other simple tests are OK for the mif. Do I need some extra option for type-checker,

Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

On Wednesday 14 October 2009 6:15:11 am Roel van Dijk wrote: > If you declare a type for f5 then ghci must check if that type is > correct, which triggers the explosion. If you don't declare a type > then it won't infer the type until necessary. Basically, ghci is lazy Well, that may be the explan

Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

On Wed, Oct 14, 2009 at 11:53 AM, Dan Doel wrote: > In fact, with GHC extensions, you don't need newtypes: >  {-# LANGUAGE LiberalTypeSynonyms #-} Ah, I completely forgot about that language extension. Thanks! > Yeah. Asking for the type of 'f4 . f4' doesn't seem to expand the synonyms, > while c

Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

On Wednesday 14 October 2009 5:25:10 am Roel van Dijk wrote: > With newtypes I can probably abstract even more. (newtype X a b = X (a (a > b)) In fact, with GHC extensions, you don't need newtypes: {-# LANGUAGE LiberalTypeSynonyms #-} type T a = (a,a) type X f a = f (f a) f0 :: a ->

Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

You can help ghci out a bit with type synonyms: type T a = (a, a) type T2 a = T (T a) type T4 a = T2 (T2 a) type T8 a = T4 (T4 a) type T16 a = T8 (T8 a) f0 :: a -> T a f1 :: a -> T2 a f2 :: a -> T4 a f3 :: a -> T8 a f4 :: a -> T16 a f0 x = (x,x) f1 = f0 . f0 f2 = f1 . f1 f3 = f2 . f2

Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

On Tuesday 13 October 2009 1:06:41 pm Brad Larsen wrote: > Good example! I have a feeling that the `dup' example is a bit > contrived, not something that one would be likely to find in the wild. This is, after all, why HM is useful. In general, there are programs that take exponential time/space

Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

On Tue, Oct 13, 2009 at 12:32 PM, Serguey Zefirov wrote: > 2009/10/13 Lennart Augustsson : >> Yes, there are simple H-M examples that are exponential. >> x0 = undefined >> x1 = (x1,x1) >> x2 = (x2,x2) >> x3 = (x3,x3) >> ... >> >> xn will have a type with 2^n type variables so it has size 2^n. > >

Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

2009/10/13 Lennart Augustsson : > Yes, there are simple H-M examples that are exponential. > x0 = undefined > x1 = (x1,x1) > x2 = (x2,x2) > x3 = (x3,x3) > ... > > xn will have a type with 2^n type variables so it has size 2^n. Reformulated: let dup x = (x,x) :t dup . dup . dup . dup ... type will

Re: [Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

ton-Jones > wrote: >> | > Is there any way to define type-level multiplication without requiring >> | > undecidable instances? >> | >> | No, not at the moment.  The reasons are explained in the paper "Type >> | Checking with Open Type Functions" (ICF

[Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

On Tue, Oct 13, 2009 at 3:37 AM, Simon Peyton-Jones wrote: > | > Is there any way to define type-level multiplication without requiring > | > undecidable instances? > | > | No, not at the moment.  The reasons are explained in the paper "Type > | Checking with Ope

Re: [Haskell-cafe] type checking that I can't figure out ....

Daniel Peebles wrote: Yeah, in a way similar to ArrowPlus/ArrowZero. Then again, I'm not sure whether it would be meaningful to split up MonadPlus like that. Well, we could always have: class MonadZero m => MonadPlus m The suggestion is just to broaden the scope of mzero so that you can have

Re: [Haskell-cafe] type checking that I can't figure out ....

Yeah, in a way similar to ArrowPlus/ArrowZero. Then again, I'm not sure whether it would be meaningful to split up MonadPlus like that. On Thu, Jun 4, 2009 at 12:40 AM, Antoine Latter wrote: > On Wed, Jun 3, 2009 at 8:52 PM, Daniel Peebles wrote: >> It seems like if we could get fail out of Mona

Re: [Haskell-cafe] type checking that I can't figure out ....

On Wed, Jun 3, 2009 at 8:52 PM, Daniel Peebles wrote: > It seems like if we could get fail out of Monad and into something > like MonadFail/Zero, then it might make sense to make a lookup that > returned an instance of that instead? > > Dan > Do you mean splitting up MonadPlus/Alternative into tw

Re: [Haskell-cafe] type checking that I can't figure out ....

It seems like if we could get fail out of Monad and into something like MonadFail/Zero, then it might make sense to make a lookup that returned an instance of that instead? Dan On Wed, Jun 3, 2009 at 8:13 PM, Bertram Felgenhauer wrote: > Michael Snoyman wrote: >> On Wed, Jun 3, 2009 at 8:42 AM,

Re: [Haskell-cafe] type checking that I can't figure out ....

Michael Snoyman wrote: > On Wed, Jun 3, 2009 at 8:42 AM, Daniel Fischer > wrote: > > Am Mittwoch 03 Juni 2009 06:12:46 schrieb Michael Snoyman: > > > 2. lookup does not return any generalized Monad, just Maybe (I think that > > > should be changed). > > > > Data.Map.lookup used to return a value i

Re: [Haskell-cafe] type checking that I can't figure out ...

True, so perhaps better written as: import Data.Maybe (fromMaybe) gets (fromMaybe (error "could not find re in resFwdMap") . M.lookup re . resFwdMap) with more detail in error message as appropriate. -Ross On Jun 3, 2009, at 5:57 PM, Henning Thielemann wrote: Ross Mellgren schrieb: You'

Re: [Haskell-cafe] type checking that I can't figure out ...

Ross Mellgren schrieb: > You've applied two solutions to get the value out -- pattern matching > (Just reinfo) and fromJust. You should use one or the other, but not both: > > -- pattern matching > remLookupFwd :: (ReVars m t) => SimplRe t -> ReM m t (ReInfo t) > remLookupFwd re >= do fwd <- g

Re: [Haskell-cafe] type checking that I can't figure out ...

You've applied two solutions to get the value out -- pattern matching (Just reinfo) and fromJust. You should use one or the other, but not both: -- pattern matching remLookupFwd :: (ReVars m t) => SimplRe t -> ReM m t (ReInfo t) remLookupFwd re = do fwd <- gets resFwdMap let { Just

[Haskell-cafe] type checking that I can't figure out ...

Hi Andrew (Bromage), I reversed the parameter order to Data.Map.lookup and calling fromJust to pull out value from Maybe wrapper ... all as you suggested: > remLookupFwd :: (ReVars m t) => SimplRe t -> ReM m t (ReInfo t) > remLookupFwd re > = do fwd <- gets resFwdMap >let { Just

Re: [Haskell-cafe] type checking that I can't figure out ....

On Wed, Jun 3, 2009 at 8:42 AM, Daniel Fischer wrote: > Am Mittwoch 03 Juni 2009 06:12:46 schrieb Michael Snoyman: > > > I made two changes: > > > > 1. You had the arguments to M.lookup backwards. > > 2. lookup does not return any generalized Monad, just Maybe (I think that > > should be changed).

Re: [Haskell-cafe] type checking that I can't figure out ....

Am Mittwoch 03 Juni 2009 06:12:46 schrieb Michael Snoyman: > I made two changes: > > 1. You had the arguments to M.lookup backwards. > 2. lookup does not return any generalized Monad, just Maybe (I think that > should be changed). Data.Map.lookup used to return a value in any monad you wanted, I

Re: [Haskell-cafe] type checking that I can't figure out ....

G'day Vasili. This should do it: remLookupFwd :: (ReVars m t) => SimplRe t -> ReM m t (ReInfo t) remLookupFwd re = do fwd <- gets resFwdMap let { Just reinfo = fromJust (M.lookup re fwd) } return reinfo The FiniteMap lookup operation took its arguments in the opposite order. Tha

Re: [Haskell-cafe] type checking that I can't figure out ....

Hi Michael, Let me look tomorrow morning. In any case, many thanks! Kind regards, Vasili On Tue, Jun 2, 2009 at 11:12 PM, Michael Snoyman wrote: > > remLookupFwd :: (ReVars m t) => SimplRe t -> ReM m t (ReInfo t) > > remLookupFwd re > > = do fwd <- gets resFwdMap > > -- let { Jus

Re: [Haskell-cafe] type checking that I can't figure out ....

> remLookupFwd :: (ReVars m t) => SimplRe t -> ReM m t (ReInfo t) > remLookupFwd re > = do fwd <- gets resFwdMap > -- let { Just reinfo = M.lookup fwd re }-- PROBLEM >reinfo <- liftMaybe $ M.lookup re fwd -- PROBLEM >return reinfo > >

[Haskell-cafe] type checking that I can't figure out ....

Hello Haskellers, I isolated to a not so small piece: > {-# OPTIONS -fglasgow-exts #-} > {-# LANGUAGE UndecidableInstances #-} > import Control.Monad.Identity > import Control.Monad.Reader > import Control.Monad.State > import qualified Data.List as L > import qualified Data.Map as M > impo

Re: [Haskell-cafe] Type checking of partial programs

So a number of people responded with various ways this is already possible. Of course GHC can already do this... it's type inference. The part I'm interested in working on is exposing the functionality in GHC's API to make this as easy as possible. -Abram _

Re: [Haskell-cafe] Type checking of partial programs

On Thu, 20 Mar 2008, Roberto Zunino wrote: ac wrote: foo :: [Foo] -> foo xs = map xs What are the possible type signatures for placeholder 1 and the possible expressions for placeholder 2? A nice GHCi trick I learned from #haskell: :t let foo xs = map ?placeholder2 xs in foo forall a

Re: [Haskell-cafe] Type checking of partial programs

You can transform this into valid Haskell98 in the following way: foo_infer xs _ | const False (xs :: [Foo]) = undefined foo_infer xs placeholder_2 = map ph xs foo xs = foo_infer xs undefined You can then do type inference on "foo_infer", giving you foo_infer :: [Foo] -> (Foo -> a) -> [a] whic

Re: [Haskell-cafe] Type checking of partial programs

zunino: > ac wrote: > > foo :: [Foo] -> > > foo xs = map xs > > > > What are the possible type signatures for placeholder 1 and the possible > > expressions for placeholder 2? > > A nice GHCi trick I learned from #haskell: > > > :t let foo xs = map ?placeholder2 xs in foo > > forall a b. (?

Re: [Haskell-cafe] Type checking of partial programs

ac wrote: > foo :: [Foo] -> > foo xs = map xs > > What are the possible type signatures for placeholder 1 and the possible > expressions for placeholder 2? A nice GHCi trick I learned from #haskell: > :t let foo xs = map ?placeholder2 xs in foo forall a b. (?placeholder2::a -> b) => [a] ->

[Haskell-cafe] Type checking of partial programs

Is anybody interested in working on this? This is a project I've been interested in for some time, but recognize I probably need some guidance before I go off and start hacking on it. As dcoutts pointed out on #haskell-soc, this may be of particular interest to people working on yi and HaRe. Other

Re: [Haskell-cafe] Type checking with Haskell

Stefan O'Rear wrote: On Thu, Apr 12, 2007 at 01:04:13PM +0100, Joel Reymont wrote: Folks, The ghc/compiler/typecheck directory holds a rather large body of code and quick browsing through did not produce any insight. How do you implement type checking in haskell? Assume I have an

Re: [Haskell-cafe] Type checking with Haskell

27;Rear wrote: Also, GHC runs typechecking *before* desugaring, apparently thinking error messages are more important than programmer sanity :) What would be the benefit of running type checking after desugaring? -- http://wagerlabs.com/ ___

Re: [Haskell-cafe] Type checking with Haskell

On 4/12/07, Joel Reymont <[EMAIL PROTECTED]> wrote: What would be the benefit of running type checking after desugaring? After desugaring, the program is written in a much more simple language (GHC Core). Type checking a desugared program is much easier because the type checker has t

Re: [Haskell-cafe] Type checking with Haskell

On Apr 12, 2007, at 3:00 PM, Stefan O'Rear wrote: Also, GHC runs typechecking *before* desugaring, apparently thinking error messages are more important than programmer sanity :) What would be the benefit of running type checking after desugaring? -- http://wagerlab

Re: [Haskell-cafe] Type checking with Haskell

er to fuse parsing and type checking in this case so that you do not need to track source positions.) I'm not sure how to do this, quite honestly. The language is dynamically typed so I have to infer variable types from their usage, function return types from what is assigned to the functi

Re: [Haskell-cafe] Type checking with Haskell

On Thu, Apr 12, 2007 at 01:04:13PM +0100, Joel Reymont wrote: > Folks, > > The ghc/compiler/typecheck directory holds a rather large body of > code and quick browsing through did not produce any insight. > > How do you implement type checking in haskell? > > Assume I

RE: [Haskell-cafe] Type checking with Haskell

] On Behalf Of Joel Reymont > Sent: 12 April 2007 13:04 > To: Haskell Cafe > Subject: [Haskell-cafe] Type checking with Haskell > > Folks, > > The ghc/compiler/typecheck directory holds a rather large body of > code and quick browsing through did not produce any insight. >

Re: [Haskell-cafe] Type checking with Haskell

On Apr 12, 2007, at 1:07 PM, Stefan Holdermans wrote: You might want to check out "Typing Haskell in Haskell" [1] by Mark P. Jones. Must be _the_ paper as Don suggested it as well. I also looked at my copy of Andrew Appel's compilers in ML book and realized that I should be going about it

Re: [Haskell-cafe] Type checking with Haskell

Joel, How do you implement type checking in haskell? You might want to check out "Typing Haskell in Haskell" [1] by Mark P. Jones. Cheers, Stefan [1] Jones, Mark P. Typing Haskell in Haskell. In Erik Meijer, editor, Proceedings of the 1999 Haskell Workshop, Friday October

[Haskell-cafe] Type checking with Haskell

Folks, The ghc/compiler/typecheck directory holds a rather large body of code and quick browsing through did not produce any insight. How do you implement type checking in haskell? Assume I have an Expr type with a constructor per type and functions can take lists of expressions. Do I

Re: [Haskell-cafe] Type checking and locating token with Parsec

without an additional type-checking pass, entirely within the > yacc grammar. I tried to take such an approach with Parsec but hit > the roadblock with buildExpressionParser since it returns the same > type as the token parser given to it. Just because you have a hammer doesn't

[Haskell-cafe] Type checking and locating token with Parsec

Folks, Imagine a language where Num + Num yields a Num and Str + Num yields a Str but Num + Str should not be allowed. I implemented parsing for such a language in OCaml with a yacc-based parser without an additional type-checking pass, entirely within the yacc grammar. I tried to take

[Haskell-cafe] powerful type checking & false expectations that a program is correct

Programmers who use languages without static type checking sometimes claim that static type checking gives folk the false impression that once the program passes type checking the program is correct. That always seemed silly to me, but I'm starting to wonder ;-) Of course, the shootout pro

Re: [Haskell-cafe] Problem type checking class-method implementation

x27;s what you get from simplifying stuff. Anyway, it seems time to have another look at the original program and maybe come with another type-checking puzzle later. ;) Thanks, Stefan http://www.cs.uu.nl/~stefan/ ___ Haskell-Cafe mailing list Ha

RE: [Haskell-cafe] Problem type checking class-method implementation

ding to the instance head, and by applying type checking constraints for functional composition, we get these types: Processor :: ProcessorT p Identity () -> Processor p () process :: process :: ( IsProcessor p (ProcessorT p Identity)

[Haskell-cafe] Problem type checking class-method implementation

Dear Haskellers, Yesterday I stumbled upon a problem type checking a program involving multi-parameter type classes. GHC rejected the program; still, I was not immediately convinced it contained a type error. Having given it some more thoughts, I start to suspect that the type checker is in

Re: Type checking

> Hi, > > Can anyone explain to me how hugs manages to derive that > > f x y z = y (y z) x > > is of type > > f :: a -> ((a -> b) -> a -> b) -> (a -> b) -> b This question was posted from an Oxford University computer; it also smells like homework. If it's genuinely not homework, Lee, I apol

Re: Type checking

On 2003-12-31 at 19:27GMT "Lee Dixon" wrote: > Hi, > > Can anyone explain to me how hugs manages to derive that > > f x y z = y (y z) x > > is of type > > f :: a -> ((a -> b) -> a -> b) -> (a -> b) -> b To begin with, f has three arguments, x y and z, so letting each of these have types Tx Ty

Type checking

Hi, Can anyone explain to me how hugs manages to derive that f x y z = y (y z) x is of type f :: a -> ((a -> b) -> a -> b) -> (a -> b) -> b Many thanks and a happy new year to all! Lee _ Stay in touch with absent friends - get M

Re: Type checking/inference

On Sun, 28 Dec 2003 04:58:12 + "Lee Dixon" <[EMAIL PROTECTED]> wrote: > Hi, > > I've run into a small problem whilst doing some manual type checking, > to see if I could match the results given by hugs > > prelude> :t foldr filter > foldr filt

Re: Type checking/inference

Lee Dixon wrote: > I've run into a small problem whilst doing some manual type checking, to see > if I could match the results given by hugs > > prelude> :t foldr filter > foldr filter :: [a] -> [a -> Bool] -> [a] > -- This was fine and was the same as my an

Re: Type checking/inference

Hi, > prelude> :t map (foldr filter) > map (foldr filter) :: [[a]] -> [[a -> Bool] -> [a]] > > Two main questions: > 1/ How does hugs derive this answer? > 2/ What input can I give so that it yields a correct result? I've tried > giving it a list of lists but it fails... Try: map (flip (foldr

Type checking/inference

Hi, I've run into a small problem whilst doing some manual type checking, to see if I could match the results given by hugs prelude> :t foldr filter foldr filter :: [a] -> [a -> Bool] -> [a] -- This was fine and was the same as my answer, so I tested it with prelude> f

Question about Type Checking

Hi i am doing a type checker. and how can i check if the Expn that i have is a Prim Function = ("f",[([Arg "x"],Simple (Int 2))]) type Function = (Name, [Equation]) type Equation = ([Expn], Body) {- (the body of) either a simple equation: f a1 .. an = e or a conditional equation: f a1 .. an | b1