search

google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

occurs check before normalization #23

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
Load this file:

<http://svn.berlios.de/viewcvs/al4nin/trunk/found-bugs/issue23-MonadPrime.omg?re
v=438&view=markup>

In the typecheck mode enter:

*** Checking: f a
*** expected type: {exch 0t _d _e}
***    refinement: (_c,0t), 
***   assumptions: 
***      theorems: 
check> :try (f a)

The typing f a :: _d
does not match the expected type:
  {exch 0t _d _e}
Because: occurs check
  _d =/= {exch 0t _d _e}

If {exch 0t _d _e} got evaluated just one step,
the equivalence whould be obvious.

(you have to comment out the last two lines to do this)

prompt> :no {exch 0t d e}

   {exch 0t a b}
Normalizes to:
  a
Refinement:

I am not sure how to handle this situation, because
the "nest" function I am trying to define looks innocent
enough (and sufficiently useful!) to typecheck.

Maybe normalization should commence in the presence of known parameters to
a certain degree, and the occurs check should kick in thereafter?

Original issue reported on code.google.com by ggr...@gmail.com on 25 Jul 2007 at 1:49

GoogleCodeExporter commented 9 years ago 
Omega Interpreter: version 1.4.2
Build Date: Thu Nov  8 15:51:28 Pacific Standard Time 2007

has a different behaviour:

**** Near line: 97 column: 1

Different types
   c ~> c ~> *0   !=   *1
(dfu ~> dfu ~> *0,*1)

Need to investigate :-)

Original comment by ggr...@gmail.com on 13 Nov 2007 at 12:56

GoogleCodeExporter commented 9 years ago 
this (i.e. comment 1) turned out to be a bug in flattenThrist.

http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue23-MonadPrime.o
mg
at revision 519 contains the corrected code.

Original comment by ggr...@gmail.com on 13 Nov 2007 at 12:53

GoogleCodeExporter commented 9 years ago 
Here is a new example:

############################
data Pat :: *2 where
  Y :: Pat
  Q :: Pat ~> Pat
 deriving Nat(p)

data Pat' :: Pat ~> *1 where
  Y' :: Pat' Y
  Q' :: Pat' n ~> Pat' (Q n)
 deriving Nat(q)

data Pat'' :: Pat' p ~> *0 where
  Y :: Pat'' Y'
  Q :: Pat'' n -> Pat'' (Q' n)
 deriving Nat(r)

plus :: Pat ~> Pat ~> Pat
{plus Y n} = n
{plus (Q m) n} = Q {plus m n}

plus' :: Pat' m ~> Pat' n ~> Pat' {plus m n}
{plus' Y' n} = n -- BUG! Occurs check
{plus' (Q' m) n} = Q' {plus' m n}
############################

I get:

(Pat Y Q) (Pat' Y' Q') (Pat'' Y Q) (plus ::plus) (plus' ::plus') Occurs check
   a   !=   {plus 0p a}
(qcb,{plus 0p qcb})

 File AutoLevelled.omg loaded.

A one-step unfolding of the plus function would restore the equality :-(

Original comment by ggr...@gmail.com on 24 Feb 2010 at 4:01

GoogleCodeExporter commented 9 years ago 
Another idea: only normalize when we have an occur. if there are any tyfun 
calls inside that can be reduced and the result passes the occur check, we can 
substitute the result for the original.

Original comment by ggr...@gmail.com on 31 Dec 2010 at 12:01

GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
issue 51 possibly related

Original comment by ggr...@gmail.com on 31 Dec 2010 at 12:22

GoogleCodeExporter commented 9 years ago 
r495. See also issue 47 and issue 51.

Original comment by ggr...@gmail.com on 3 Jan 2011 at 4:12

GoogleCodeExporter commented 9 years ago 
r502 should fix the ":try f a" problem from comment 2.
I think there are no more residual problems in this issue.

Original comment by ggr...@gmail.com on 4 Jan 2011 at 2:45