This was already featured in the Weekly News a couple of weeks back, but I think maybe it deserves it’s own thread. I’ve tried to explain this approach to some people before, but I think this article does a much better job than I have.

I do think the “Defeating” in the title might be a little bit negative, it’s have preferred something neutral like “When your result type depends on your argument values”, but it’s still something useful to know from retaining your type safety.

This existentials and GADTs can be converted into a CPS style without type equality constraints (usually, with enough work) so that you can start from this description but use it in languages with less sophisticated type systems – as long as they have parametricity – like Haskell 2010.

  • jaror@kbin.social
    link
    fedilink
    arrow-up
    1
    ·
    1 year ago

    This gives a nice practical motivation for GADTs and existential quantification.

    This existentials and GADTs can be converted into a CPS style without type equality constraints

    That sounds interesting. I can’t easily imagine what that would look like. Do you have an example?

    • Boyd Stephen Smith Jr.@hachyderm.io
      link
      fedilink
      arrow-up
      2
      ·
      1 year ago

      @jaror @bss03 Maybe I was wrong, but I think you can do Scott encoding of the GADT underneath the standard codensity representation of existentials via CPS. Still need higher-rank types, not “just” parametricity.

      I should write up some code to check myself against GHC.

    • bss03@infosec.pubOP
      link
      fedilink
      English
      arrow-up
      1
      ·
      edit-2
      1 year ago

      I put this together this evening.

      {-# language GADTs #-}
      {-# language RankNTypes #-}
      
      import Data.Functor.Const
      
      -- The GADT
      data AGADT a where
          I :: [Integer] -> AGADT Integer
          S :: String -> AGADT String
      
      type Scott_GADT a = forall fr. ([Integer] -> fr Integer) -> (String -> fr String) -> fr a
      
      f :: AGADT a -> String
      f (I x) = show x
      f (S x) = x
      
      f' :: Scott_GADT a -> String
      f' x = getConst $ x (Const . show) Const
      
      -- The Existential
      data AnyGADT = forall a. MkAnyGADT (AGADT a)
      
      type Scott_Any =
        forall r.
          (forall a. (forall fr. ([Integer] -> fr Integer) -> (String -> fr String) -> fr a) -> r) ->
          r
      
      g :: String -> AnyGADT
      g "foo" = MkAnyGADT (I [42])
      g "bar" = MkAnyGADT (I [69])
      g x = MkAnyGADT (S x)
      
      g' :: String -> Scott_Any
      g' "foo" x = x (\i _s -> i [42])
      g' "bar" x = x (\i _s -> i [69])
      g' s x = x (\_i s' -> s' s)
      
      main = interact (unlines . fmap x . lines)
       where
        x s = case g s of { MkAnyGADT x -> f x }
        y s = g' s f'
      

      You can swap out x for y to see the behavior is the same.

      You can drop the GADT pragma, GADT definition, f, existential, g, and x (but keep all the Scott versions, includeing y) to reveal code that works “simply” with RankNTypes.

      Higher-rank types and parametricity is quite powerful.

      BTW, this isn’t new / doesn’t require the bleeding edge compiler. I’m on “The Glorious Glasgow Haskell Compilation System, version 9.0.2” from the Debian repositories.

      • jaror@kbin.social
        link
        fedilink
        arrow-up
        1
        ·
        1 year ago

        The Lemmy->Kbin conversion has inserted a lot of <span> elements into your code making it unreadable. For people reading this from the Kbin side, here’s the code:

        {-# language GADTs #-}
        {-# language RankNTypes #-}
        
        import Data.Functor.Const
        
        -- The GADT
        data AGADT a where
            I :: [Integer] -> AGADT Integer
            S :: String -> AGADT String
        
        type Scott_GADT a = forall fr. ([Integer] -> fr Integer) -> (String -> fr String) -> fr a
        
        f :: AGADT a -> String
        f (I x) = show x
        f (S x) = x
        
        f' :: Scott_GADT a -> String
        f' x = getConst $ x (Const . show) Const
        
        -- The Existential
        data AnyGADT = forall a. MkAnyGADT (AGADT a)
        
        type Scott_Any =
          forall r.
            (forall a. (forall fr. ([Integer] -> fr Integer) -> (String -> fr String) -> fr a) -> r) ->
            r
        
        g :: String -> AnyGADT
        g "foo" = MkAnyGADT (I [42])
        g "bar" = MkAnyGADT (I [69])
        g x = MkAnyGADT (S x)
        
        g' :: String -> Scott_Any
        g' "foo" x = x (\i _s -> i [42])
        g' "bar" x = x (\i _s -> i [69])
        g' s x = x (\_i s' -> s' s)
        
        main = interact (unlines . fmap x . lines)
         where
          x s = case g s of { MkAnyGADT x -> f x }
          y s = g' s f'
        
        ```</span>
        • bss03@infosec.pubOP
          link
          fedilink
          arrow-up
          1
          ·
          edit-2
          1 year ago

          I think the spans are all syntax highlighting/coloring. Your comment seems to have a dangling ```/span at the end to me, but that might just be the KBin->Lemmy translation.

          EDIT: Also, Lemmy seems to be munging this post between the preview and the submit, due to me wanting to include some text that appears to be a dangling xml/html end tag (angle brackets removed in edit for “readability”) inside backticks.

      • jaror@kbin.social
        link
        fedilink
        arrow-up
        1
        ·
        1 year ago

        Ah, that’s interesting. Although I can imagine not many people would want to write code in that style. And I also wonder how many languages support higher rank polymorphism in the first place.

        • bss03@infosec.pubOP
          link
          fedilink
          arrow-up
          1
          ·
          1 year ago

          Yeah, I generally prefer pattern matching and constructor calls, but often languages don’t have GADTs or existentials. Even in GHC, existentials are still a bit “wonky”, though still generally nicer to use than CPS/Codensity.

  • lukewarm@kbin.social
    link
    fedilink
    arrow-up
    1
    ·
    1 year ago

    This is probably a stupid question, but what does this trickery with GADTs and Existential Types give compared to the “normal” way?

    import Data.Int (Int8, Int16)
    import Data.ByteString (ByteString)
    
    data ParsedImage
      = ParsedAs8 (Int, Int, [Int8])
      | ParsedAs16 (Int, Int, [Int16])
      deriving Show
    
    parseImage :: ByteString -> ParsedImage
    parseImage = undefined
    
    imageDimensions :: ByteString -> (Int, Int)
    imageDimensions str =
      case parseImage str of
        ParsedAs8 (w, h, _) -> (w, h)
        ParsedAs16 (w, h, _) -> (w, h)
    
    

    Basically, the same way as a function can return an Either and everyone is happy to pattern-match on the result.

    • bss03@infosec.pubOP
      link
      fedilink
      English
      arrow-up
      0
      ·
      1 year ago

      The GADT allows some constructors to be safely unhandled when the type parameter is known.

      The consuming a ParsedImage, you always have to deal with both constructors. When consuming a Image px or an AnyImage, you also have to deal with both Image constructors. When consuming a Image Pixel8Bit the type system proves that it couldn’t be constructed with the Image16Bit constructor, so you only have to deal with the Image8Bit constructor.

      HTH

      • lukewarm@kbin.social
        link
        fedilink
        arrow-up
        1
        ·
        1 year ago

        But how? Parsing function can return any of the types, we don’t know what was in the bytestring. So we’d need to deal with all variations in any case, no?

        Is the difference in that it becomes possible to pattern-match on a type of an element inside the structure, rather than on the structure as a whole? So as long as you don’t need that element, you can access elements that are common without pattern-matching? I guess it’s a marginal benefit…

        Or do I still misunderstand?

        • bss03@infosec.pubOP
          link
          fedilink
          arrow-up
          0
          ·
          1 year ago

          Parsing function can return any of the types, we don’t know what was in the bytestring. So we’d need to deal with all variations in any case, no?

          Yes, the parsing function could return anything, but that’s not the exclusive source of values of the GADT.

          So, yes, when consuming the output of the parsing function, you have to deal with all the variations. But, when you have types that reflect some information is known about the type index, you only have to deal with the matching constructors.

          This is particularly important given the copy-paste transport of code from one context to another. You might have some code that works for a MyGADT MyType and doesn’t handle all the constructors. But, when you transport that code elsewhere and ask it to handle a MyGADT a, the type system will correctly warn you that you haven’t handled all the cases. This is an improvement over writing something like case x of { Right y -> stuff y; Left{} -> error "Can't happen; won't happen"; }, since I’m sure works fine in the right context, but doesn’t have a type that reflects what the programmer knows about x so if it is transported to a context where that information/assumption is no longer true, that’s only discovered at runtime. (This isn’t the best example, but it’s what I have for you.)

          • lukewarm@kbin.social
            link
            fedilink
            arrow-up
            1
            ·
            1 year ago

            Well, I guess that I can see the value… Leaving copy-pasting problem aside, you might, for instance, want to have a type for a message with moderately complex envelope and a wide variety of possible payload types. It would be useful to have functions that act on the envelope, and treat payload as something opaque.

            Thanks for the conversation!