#9637 closed feature request (fixed)
Type level programming needs an error function
Reported by: | augustss | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.0.1 |
Component: | Compiler | Version: | 7.8.3 |
Keywords: | Cc: | adamgundry | |
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: |
Description (last modified by )
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: Proposal/CustomTypeErrors
Change History (14)
comment:1 Changed 4 years ago by
comment:2 Changed 4 years ago by
I'll experiment and see what seems to work well in the Mu compiler.
comment:3 Changed 4 years ago by
Here's what I'm using now, and it works nicely. But better names would be nice.
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:
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.
comment:4 Changed 4 years ago by
Can you give some examples of its use in a program? I still don't get it.
comment:5 Changed 4 years ago by
Here's a real example:
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)
comment:6 Changed 4 years ago by
Cc: | adamgundry added |
---|
comment:7 Changed 4 years ago by
Related Tickets: | → #9180, #9636 |
---|
comment:8 Changed 3 years ago by
Description: | modified (diff) |
---|---|
Differential Rev(s): | → Phab:D1236 |
comment:9 Changed 3 years ago by
On the implementation front, I have some suggestions, which I've added under SLPJ alternative design
on the wiki page CustomTypeErros
(The title of the wiki page is mis-spelled. Rename?)
comment:10 Changed 3 years ago by
Description: | modified (diff) |
---|---|
Milestone: | → 8.0.1 |
It sounds like this will make it in for 8.0.1 with an implementation by Iavor Diatchki. Thanks Iavor!
comment:12 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
comment:13 Changed 3 years ago by
I embellished the documentation a bit in 568736d757d3e0883b0250e0b948aeed646c20b5.
comment:14 Changed 3 years ago by
I just want to add: The Helium people also thought about customizing error messages: See Heeren, Hage, Swierstra on Scripting the Type Inference Process.
I'm all for it! Can you write a more precise specification?
Simon