Replying to [comment:26 DerekElkins]:
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
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
#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 DerekElkins): Replying to [comment:28 jonsterling]: 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.) Yeah, in my reply on Richard Eisenberg's blog post,https://typesandkinds.wordpress.com/2015/09/09/what-are-type- families/, I explicitly introduce codes. I don't ''think'' this really changes the picture. (If this does, I'd like to know. Specifically if viewing (closed) type families as functions on codes of types that get interpreted into functions on types misses something important due to being limited to codes.) 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. I agree, in CTT `f(m)` is definitely not canonical and nothing like the generative view I suggested. I mainly mentioned CTT as I think it provides an interesting perspective. Frankly, the behavior Lennart is complaining about is the behavior I expected a priori. My suggestion is essentially that codes for * are being quotiented. The mention of HITs was simply because I still really want codes to be "inductive". I go into this further on the above mentioned blog reply where I've also no doubt said at best imprecise things about CTT (though not they are not relevant to this approach.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler