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.