Opened 3 years ago
Last modified 21 months ago
#395 new feature
Better inference for effectful case expressions.
Reported by: | benl | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Source Typing | Version: | 0.4.2 |
Keywords: | Cc: |
Description (last modified by benl)
In this function the result computation is boxed in both alternatives, we means we must weaken the effect of the first one so that the types match.
module Test where data List (a : Data) where Nil : List a Cons : a -> List a -> List a mapS [a b : Data] [e : Effect] (f : a -> S e b) (xx : List a) : S e (List b) = case xx of Nil -> box (weakeff [e] in Nil) Cons x xs -> box (Cons (run f x) (run mapS f xs))
Change History (4)
comment:1 Changed 3 years ago by benl
- Description modified (diff)
comment:2 Changed 3 years ago by benl
- Milestone 0.4.3 deleted
comment:3 Changed 21 months ago by benl
- Component changed from Source Type Inferencer to Source Typing
comment:4 Changed 21 months ago by benl
- Type changed from enhancement to feature
Note: See
TracTickets for help on using
tickets.