[GHC] #9637: Type level programming needs an error function
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- When doing type level programming you often need a way to report errors. I suggest a closed type family called Error with special semantics. It is kinded like this Error :: Symbol -> k1 -> k2 If this function has to be reduced during constraint solving it will simply generate a type error with the given string and printing the type as extra information (this kind can be generalized a lot if we want to). I've found that having this function gives more accurate and earlier error messages. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm all for it! Can you write a more precise specification? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by augustss): I'll experiment and see what seems to work well in the Mu compiler. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by augustss): Here's what I'm using now, and it works nicely. But better names would be nice. {{{#!hs type family Error (a :: k1) :: k2 where { } data ErrorAnd (a :: k1) (b :: k2) }}} When the type checker encounters the Error function it generates the error message according to the following pseudo code: {{{#!hs flatten (Symbol s) = s flatten (ErrorAnd t1 t2) = flatten t1 ++ flatten t2 flatten t = prettyPrint t }}} So for instance `Error "Oh noes!"` will generate the error message "Oh noes!". And {{{Error ("Mismatch between " `ErrorAnd` t1 `ErrorAnd` " and " `ErrorAnd` t2)}}} will generate "Mismatch between ... and ...", where ... are the pretty printing of the types t1 and t2 respectively. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Can you give some examples of its use in a program? I still don't get it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by augustss): Here's a real example: {{{#!hs type F_NoDups (t :: FieldSet) :: FieldSet = Assert "Type has duplicate labels:\n " (Not (F_HasDups t)) t type family Assert (msg :: Symbol) (a :: Bool) (b :: k) :: k where Assert msg True x = x Assert msg False x = Error (msg `ErrorAnd` x) }}} And here's a sample error message: {{{ RunMu.exe: Cortex: Cortex.Stem.Relation.Test.Typed:21:1: Type error: Type has duplicate labels: Cortex.Stem.Relation.Types.FS ("A" ::: String : "B" ::: Bool : "B" ::: Bool : "C" ::: () : Data.TypeLevel.Nil) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #9180, #9636 | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * related: => #9180, #9636 Comment: #9180 proposes a similar mechanism at the term level. #9636 is a nice application of the feature proposed in this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | 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: #9180, #9636 | Differential Revisions: Phab:D1236 -------------------------------------+------------------------------------- Changes (by simonpj): * differential: => Phab:D1236 Old description:
When doing type level programming you often need a way to report errors. I suggest a closed type family called Error with special semantics. It is kinded like this Error :: Symbol -> k1 -> k2
If this function has to be reduced during constraint solving it will simply generate a type error with the given string and printing the type as extra information (this kind can be generalized a lot if we want to).
I've found that having this function gives more accurate and earlier error messages.
New description: When doing type level programming you often need a way to report errors. I suggest a closed type family called Error with special semantics. It is kinded like this Error :: Symbol -> k1 -> k2 If this function has to be reduced during constraint solving it will simply generate a type error with the given string and printing the type as extra information (this kind can be generalized a lot if we want to). I've found that having this function gives more accurate and earlier error messages. Wiki design page: [wiki:CustomTypeErros] -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | 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: #9180, #9636 | Differential Revisions: Phab:D1236 -------------------------------------+------------------------------------- Comment (by simonpj): On the implementation front, I have some suggestions, which I've added under `SLPJ alternative design` on the wiki page [wiki:CustomTypeErros] (The title of the wiki page is mis-spelled. Rename?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 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: #9180, #9636 | Differential Rev(s): Phab:D1236 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: => 8.0.1 Old description:
When doing type level programming you often need a way to report errors. I suggest a closed type family called Error with special semantics. It is kinded like this Error :: Symbol -> k1 -> k2
If this function has to be reduced during constraint solving it will simply generate a type error with the given string and printing the type as extra information (this kind can be generalized a lot if we want to).
I've found that having this function gives more accurate and earlier error messages.
Wiki design page: [wiki:CustomTypeErros]
New description: When doing type level programming you often need a way to report errors. I suggest a closed type family called Error with special semantics. It is kinded like this Error :: Symbol -> k1 -> k2 If this function has to be reduced during constraint solving it will simply generate a type error with the given string and printing the type as extra information (this kind can be generalized a lot if we want to). I've found that having this function gives more accurate and earlier error messages. Wiki design page: [wiki:Proposal/CustomTypeErrors] -- Comment: It sounds like this will make it in for 8.0.1 with an implementation by Iavor Diatchki. Thanks Iavor! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function
-------------------------------------+-------------------------------------
Reporter: augustss | Owner:
Type: feature request | Status: new
Priority: normal | Milestone: 8.0.1
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: #9180, #9636 | Differential Rev(s): Phab:D1236
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.8.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9180, #9636 | Differential Rev(s): Phab:D1236 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.8.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9180, #9636 | Differential Rev(s): Phab:D1236 Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): I embellished the documentation a bit in 568736d757d3e0883b0250e0b948aeed646c20b5. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9637: Type level programming needs an error function -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.8.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9180, #9636 | Differential Rev(s): Phab:D1236 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Lemming): I just want to add: The Helium people also thought about customizing error messages: See Heeren, Hage, Swierstra on [http://www.staff.science.uu.nl/~hage0101/scriptingthetypeinferencer.pdf Scripting the Type Inference Process]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9637#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC