Possible places of Constraints inside types

#21

Thanks for the response here and the follow up below! I think I understand a little bit more about how subsumption works now, and why I see the (to me) odd behavior.

#22

While you’re rebuilding your brain, here’s an interesting thing to think about (this uses the new visible type applications in PureScript 0.15.10, but it could easily be adapted not to):

class Amphibian a where
  frogOrToad :: forall z. (Frog a => z) -> (Toad a => z) -> z

class Frog a where
  ribbit :: a -> String

class Toad a where
  croak :: a -> String


instance Amphibian Int where
  frogOrToad ifFrog _ = ifFrog
  
instance Frog Int where
  ribbit a = "ribbit: " <> show a

instance Amphibian String where
  frogOrToad _ ifToad = ifToad

instance Toad String where
  croak a = "croak: " <> a

speak :: forall a. Amphibian a => a -> String
speak a = frogOrToad @a (ribbit a) (croak a)

main :: Effect Unit
main = do
  log $ speak 500
  log $ speak "hi"

Note the placement of the Frog a => and Toad a => constraints. They both appear in frogOrToad, but not as constraints on the types a can take at the point where a is quantified (after all, there is no type in this example that is both Frog and Toad!). But they do still do important work where they are; they participate in a claim that every Amphibian a is either a Frog or a Toad, making Amphibian sort of like a sealed class in an OO language, or like a named disjunction of Frog and Toad.

This example is silly, but the technique of expressing a disjunction of classes like this has more serious applications. Unlike Partial, which is weirder to reason about because it’s nullary (is there a Partial instance out there or isn’t there, one might wonder), these classes might give you some useful points for your intuition to grab onto.

3 Likes
A function with type variable Coercible to one of 2 types
#23

For slightly further mind bending, consider that speak could also be eta-reduced (kind of):

speak :: forall a. Amphibian a => a -> String
speak = frogOrToad @a ribbit croak

So that z ~ (a -> String)

#24

Off topic, but I wanted to say as a hobbyist, these sorts dialectical forum posts are my favorite way to learn some of the intricacies of the type system. :slight_smile:

I tend to grok this stuff best when I find a use for it in my own code, but I’ve gotten my feet under me fairly well over the past year or so just from PS by Example and all the awesome long-form answers given here.

So… thanks!

1 Like