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.

  • 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.