google-code-export / omega

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

type functions' names are also added into value namespace #71

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
try:

#########
foo a = a

foo :: Nat ~> Nat
{foo n} = n
#########

You'll see a redefinition error. But the type function should be in the type 
namespace only, and 
shouldn't contaminate the value namespace! Just like data types vs. data 
constructor functions (at 
level 0).

Original issue reported on code.google.com by ggr...@gmail.com on 24 Feb 2010 at 10:14

GoogleCodeExporter commented 9 years ago

Original comment by ggr...@gmail.com on 3 Feb 2011 at 11:09

GoogleCodeExporter commented 9 years ago
Index: Syntax.hs
===================================================================
--- Syntax.hs   (revision 706)
+++ Syntax.hs   (working copy)
@@ -1048,8 +1048,10 @@
 freeOfDec :: Dec -> ([Var],[Var])
 freeOfDec d = (bound,deps)
   where x = vars [] [d] emptyF
-        bound = binds x ++ map flagNm (filter (not . typVar) (tbinds x))
-        deps = free x ++ depends x ++ map flagNm (tfree x)
+        flagBind v | isTypeFun d = flagNm v
+        flagBind v = v
+        bound = map flagBind (binds x) ++ map flagNm (filter (not . typVar) 
(tbinds x))
+        deps = map flagBind (free x) ++ map flagBind (depends x) ++ map flagNm 
(tfree x)

 flagNm (Global x) = Global("%"++x)
 flagNm (Alpha x nm) = Alpha ("%"++x) nm

Original comment by ggr...@gmail.com on 3 Feb 2011 at 3:50

GoogleCodeExporter commented 9 years ago
r710 and r711 are the beginnings of a compelling solution (I am doing this on a 
branch because of the imminent release).

Original comment by ggr...@gmail.com on 4 Feb 2011 at 12:21

GoogleCodeExporter commented 9 years ago
branches/issue71 contains a working solution now (r717)

But we should consider extending Var by a new branch: (GlobalTy nm).

So I suggest to merge this branch and continue with the GlobalTy idea. For 
level universal (data) constructors we may have to do an extra dance, as they 
are both value and type namespace affecting.

Original comment by ggr...@gmail.com on 4 Feb 2011 at 2:15

GoogleCodeExporter commented 9 years ago
Merged with r719. For the rest of the works we should create a new branch.

Original comment by ggr...@gmail.com on 4 Feb 2011 at 3:29

GoogleCodeExporter commented 9 years ago
Maybe instead of introducing GlobalTy one should diversify Name:
type-only
value-only
type-or-value (level universal data constr).

Anyway this will be a big(gish) work, maybe we would fare better by leaving in 
the flagged hack. Anyway, post-1.5 ...

Original comment by ggr...@gmail.com on 4 Feb 2011 at 3:40