tag:blogger.com,1999:blog-11295132.post4864434678468834247..comments2017-12-12T08:09:30.941-08:00Comments on A Neighborhood of Infinity: Constraining Types with Regular ExpressionsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger16125tag:blogger.com,1999:blog-11295132.post-78476541425802753722017-07-12T21:49:20.283-07:002017-07-12T21:49:20.283-07:00The link to McBride's paper on dissections is ...The link to McBride's paper on dissections is dead. The paper can be found at <a href="https://personal.cis.strath.ac.uk/conor.mcbride/Dissect.pdf" rel="nofollow">his University of Strathclyde site</a>.David Feuerhttps://www.blogger.com/profile/09876399378889159844noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-67697894178902934112012-06-15T18:31:38.323-07:002012-06-15T18:31:38.323-07:00> The error message is due to the other annoyan...> The error message is due to the other annoyance I'm having with ghc: I don't know how to make it fully reduce types in its error messages.<br /><br />In GHCi 7.4 there is a :kind! command that reduces a type.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-2095553834006481042011-05-31T23:46:20.213-07:002011-05-31T23:46:20.213-07:00(i keep posting here since i don't
know your ...(i keep posting here since i don't <br />know your email)<br /><br />This[1] version typechecks, it seems the positivity checker can't see through the module boundary, maybe it'd pay to use "Indexed Containers"[2].<br /><br />[1]http://code.haskell.org/~Saizan/RegularTypes.agda<br />[2]http://www.cs.nott.ac.uk/~txa/publ/ICont.pdfSaizanhttps://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-4760428271383167932011-05-29T19:23:45.333-07:002011-05-29T19:23:45.333-07:00here's the example on how one usually avoids t...here's the example on how one usually avoids the --no-positivity-check flag: http://code.haskell.org/~Saizan/UCodes.agda<br /><br />Desc is a datatype of descriptions for plain polynomial functors, but i see in the post you already have Hom for your functors, which is pretty close to what you'd need.Saizanhttps://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-83503327137687088442010-08-16T15:27:58.783-07:002010-08-16T15:27:58.783-07:00Saizan,
Thanks for the agda version. It'll he...Saizan,<br /><br />Thanks for the agda version. It'll help me to learn the language.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-18354777942152298152010-08-16T11:26:42.468-07:002010-08-16T11:26:42.468-07:00Nice. It seems this scheme could not only be but u...Nice. It seems this scheme could not only be but used to restrict data in a regular fashion (trees, etc) but also code (monadic operations, protocol sequences, etc.). I.e. here another excercise: apply this scheme to model "session types".heckenpenner_rothttps://www.blogger.com/profile/11645785715024119039noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-21730317678226375862010-08-16T04:57:45.742-07:002010-08-16T04:57:45.742-07:00As for the bug i think it's the same problem a...As for the bug i think it's the same problem as http://hackage.haskell.org/trac/ghc/ticket/3500 , i've left a comment there.Saizanhttps://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-26302710975468485132010-08-16T03:19:44.351-07:002010-08-16T03:19:44.351-07:00"((),Fix (S Zero, Zero) (K22 (x, ()) (Void, x..."((),Fix (S Zero, Zero) (K22 (x, ()) (Void, x)) (I :+: (X :*: Y)))" won't really reduce to Void, since (,) is a type constructor, but assuming totality and that Fix is a least fixed point we can show that it's isomorphic to it, like in this Agda version:<br />http://hpaste.org/fastcgi/hpaste.fcgi/view?id=29142#a29142Saizanhttps://www.blogger.com/profile/07314943153376710289noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-42996422521275991652010-08-15T17:28:23.525-07:002010-08-15T17:28:23.525-07:00Oh, I misunderstood. The code *is* passing my test...Oh, I misunderstood. The code *is* passing my tests. The error message is due to the other annoyance I'm having with ghc: I don't know how to make it fully reduce types in its error messages. That type *is* Void, once fully reduced.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-39093233259278578732010-08-15T17:17:43.147-07:002010-08-15T17:17:43.147-07:00Sjoerd,
Ow! I actually checked that, and kept che...Sjoerd,<br /><br />Ow! I actually checked that, and kept checking, just the way you did. Unfortunately -fwarn-inplete-pattern and -XEmptyDecls don't play well together and so you test if the code is correct by getting it to generate an error (and conversely as you've found). So I hope it's just a typo that happened during the renaming and reformatting I did at the end. Haven't got time to look into right now...sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-26682136608412010972010-08-15T13:51:49.596-07:002010-08-15T13:51:49.596-07:00Something is not right. You say:
> iso1' (...Something is not right. You say:<br /><br />> iso1' (Fix (Right (Right a))) = error "Can't be called as a is void"<br /><br />But if I replace a with '?' ghc says:<br /><br />Couldn't match expected type `((),<br /> Fix (S Zero, Zero) (K22 (x, ()) (Void, x)) (I :+: (X :*: Y)))'<br /> against inferred type `Char'<br /><br />That's not Void!Sjoerd Visscherhttps://www.blogger.com/profile/10698430967044536619noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-31422768031650624772010-08-15T08:49:59.005-07:002010-08-15T08:49:59.005-07:00The matrices are easily generizable to Brents type...The matrices are easily generizable to Brents type lists:<br /><br />> type instance (x ::: xs) :! (i, j) = ((x ::: xs) :!! i) :!! j<br />> type instance Dim Nil = Zero<br />> type instance Dim (x ::: xs) = S (Dim xs)<br /><br />You can get K22 back as a type family:<br /><br />> type family K22 row0 row1 :: *<br />> type instance K22 (m00, m01) (m10, m11) = <br />> ((m00 ::: m01 ::: Nil) ::: <br />> (m10 ::: m11 ::: Nil) ::: Nil)Sjoerd Visscherhttps://www.blogger.com/profile/10698430967044536619noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-39562333846604134302010-08-15T08:43:24.144-07:002010-08-15T08:43:24.144-07:00Well you can't define List' this way witho...Well you can't define List' this way without a version of List coming out too :-) Hope it all still makes some kind of sense.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-43006898197502241752010-08-15T08:33:32.996-07:002010-08-15T08:33:32.996-07:00I found it a bit confusing that you used D in the ...I found it a bit confusing that you used D in the definition of List. I guess it was just an example.<br /><br />type List x = Fix (I0, I0) (K11 x) ListF works as well for the obvious definition of K11, with a level of Either a Void less in the values.Sjoerd Visscherhttps://www.blogger.com/profile/10698430967044536619noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-59583548553042783602010-08-15T07:53:08.263-07:002010-08-15T07:53:08.263-07:00Thanks for putting in the work to isolate the prob...Thanks for putting in the work to isolate the problem. You going to report it?sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-49076630833449379422010-08-15T04:38:47.523-07:002010-08-15T04:38:47.523-07:00I think you've found a bug in the construction...I think you've found a bug in the construction of circular typeclass dictionaries when type families are involved.<br /><br /><br />{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances #-}<br /><br />newtype Mu1 f = Mu1 (f (Mu1 f))<br />instance Show (f (Mu1 f)) => Show (Mu1 f) where<br /> show (Mu1 f) = show f<br /><br />newtype Mu2 f = Mu2 (f (Mu2 f)) -- same as Mu1 <br />type family Id m <br />type instance Id m = m<br />instance Show (Id (f (Mu2 f))) => Show (Mu2 f) where<br /> show (Mu2 f) = show f<br /><br /><br />{- <br />*Main> show (Mu2 $ Left ()) <br /> C-c C-cInterrupted. <br />*Main> show (Mu1 $ Left ()) <br />"Left ()" <br />*Main> <br />-}Saizanhttps://www.blogger.com/profile/07314943153376710289noreply@blogger.com