#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by jonsterling): Replying to [comment:26 DerekElkins]:
This is a fun one. We can look at what some other systems do in similar situations.
comment:17 talks about handling unevaluated terms and the discussion has been talking about partial functions. One system that deals in this realm is Computational Type Theory (CTT), the type theory underlying NuPRL (and now JonPRL). In NuPRL you can literally write the equivalent of:
{{{#!hs T Int = Bool T x = fix id }}}
thanks for the shoutout! I just thought I would clarify that, whilst in the past it was considered and perhaps experimented with, Nuprl does not currently have the ability to perform case analysis on types. (However, one of the principle reasons for types having an intensional equality in Nuprl rather than the standard extensional one is to not rule out the option of providing an eliminator to the universe in the future.) Anyway—with regard to partial operations, you are correct that it is not really a problem in Nuprl or JonPRL if a definition is partial; reduction is guided by the user in Nuprl. (By the way, contrary to oft-repeated mythology, it *is* safe to reduce terms in any context in CTT/ETT—this is guaranteed by the fact that computational equivalence is a congruence, a well-known result that comes from Howe.) It is *not* the case that for some function `f` and value `m`, `f(m)` is stuck (or worse, "canonical") if `f` is not defined at `m`; instead, it diverges. So viewing Haskell-style type families (whether open or closed) as functions or operations doesn't really work, though I believe that in many cases where a Haskell programmer reaches for a type family, they are really wanting a function/operation. I like your view of type families as generative in the same sense as data families, but quotiented by further axioms. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler