bss03, 7 months ago (edited 7 months ago)

I put this together this evening.

<span style="color:#323232;">{-# language GADTs #-}
</span><span style="color:#323232;">{-# language RankNTypes #-}
</span><span style="color:#323232;">
</span><span style="font-weight:bold;color:#a71d5d;">import </span><span style="color:#323232;">Data.Functor.Const
</span><span style="color:#323232;">
</span><span style="font-style:italic;color:#969896;">-- The GADT
</span><span style="font-weight:bold;color:#a71d5d;">data </span><span style="color:#0086b3;">AGADT</span><span style="color:#323232;"> a </span><span style="font-weight:bold;color:#a71d5d;">where
</span><span style="color:#323232;">    </span><span style="color:#0086b3;">I </span><span style="font-weight:bold;color:#a71d5d;">::</span><span style="color:#323232;"> [</span><span style="color:#0086b3;">Integer</span><span style="color:#323232;">] </span><span style="font-weight:bold;color:#a71d5d;">-> </span><span style="color:#0086b3;">AGADT Integer
</span><span style="color:#323232;">    </span><span style="color:#0086b3;">S </span><span style="font-weight:bold;color:#a71d5d;">:: </span><span style="color:#0086b3;">String </span><span style="font-weight:bold;color:#a71d5d;">-> </span><span style="color:#0086b3;">AGADT String
</span><span style="color:#323232;">
</span><span style="font-weight:bold;color:#a71d5d;">type </span><span style="color:#0086b3;">Scott_GADT</span><span style="color:#323232;"> a </span><span style="font-weight:bold;color:#a71d5d;">=</span><span style="color:#323232;"> forall fr</span><span style="font-weight:bold;color:#a71d5d;">.</span><span style="color:#323232;"> ([</span><span style="color:#0086b3;">Integer</span><span style="color:#323232;">] </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> fr </span><span style="color:#0086b3;">Integer</span><span style="color:#323232;">) </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> (</span><span style="color:#0086b3;">String </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> fr </span><span style="color:#0086b3;">String</span><span style="color:#323232;">) </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> fr a
</span><span style="color:#323232;">
</span><span style="font-weight:bold;color:#795da3;">f </span><span style="font-weight:bold;color:#a71d5d;">:: AGADT </span><span style="color:#323232;">a </span><span style="font-weight:bold;color:#a71d5d;">-> String
</span><span style="color:#323232;">f (I x) </span><span style="font-weight:bold;color:#a71d5d;">= </span><span style="color:#323232;">show x
</span><span style="color:#323232;">f (</span><span style="color:#0086b3;">S</span><span style="color:#323232;"> x) </span><span style="font-weight:bold;color:#a71d5d;">=</span><span style="color:#323232;"> x
</span><span style="color:#323232;">
</span><span style="font-weight:bold;color:#795da3;">f' </span><span style="font-weight:bold;color:#a71d5d;">:: Scott_GADT </span><span style="color:#323232;">a </span><span style="font-weight:bold;color:#a71d5d;">-> String
</span><span style="color:#323232;">f' x </span><span style="font-weight:bold;color:#a71d5d;">= </span><span style="color:#323232;">getConst </span><span style="font-weight:bold;color:#a71d5d;">$</span><span style="color:#323232;"> x (</span><span style="color:#0086b3;">Const </span><span style="font-weight:bold;color:#a71d5d;">.</span><span style="color:#323232;"> show) </span><span style="color:#0086b3;">Const
</span><span style="color:#323232;">
</span><span style="font-style:italic;color:#969896;">-- The Existential
</span><span style="font-weight:bold;color:#a71d5d;">data </span><span style="color:#0086b3;">AnyGADT </span><span style="font-weight:bold;color:#a71d5d;">=</span><span style="color:#323232;"> forall a</span><span style="font-weight:bold;color:#a71d5d;">. </span><span style="color:#0086b3;">MkAnyGADT</span><span style="color:#323232;"> (</span><span style="color:#0086b3;">AGADT</span><span style="color:#323232;"> a)
</span><span style="color:#323232;">
</span><span style="font-weight:bold;color:#a71d5d;">type </span><span style="color:#0086b3;">Scott_Any </span><span style="font-weight:bold;color:#a71d5d;">=
</span><span style="color:#323232;">  forall r</span><span style="font-weight:bold;color:#a71d5d;">.
</span><span style="color:#323232;">    (forall a</span><span style="font-weight:bold;color:#a71d5d;">.</span><span style="color:#323232;"> (forall fr</span><span style="font-weight:bold;color:#a71d5d;">.</span><span style="color:#323232;"> ([</span><span style="color:#0086b3;">Integer</span><span style="color:#323232;">] </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> fr </span><span style="color:#0086b3;">Integer</span><span style="color:#323232;">) </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> (</span><span style="color:#0086b3;">String </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> fr </span><span style="color:#0086b3;">String</span><span style="color:#323232;">) </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> fr a) </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> r) </span><span style="font-weight:bold;color:#a71d5d;">->
</span><span style="color:#323232;">    r
</span><span style="color:#323232;">
</span><span style="font-weight:bold;color:#795da3;">g </span><span style="font-weight:bold;color:#a71d5d;">:: String -> AnyGADT
</span><span style="color:#323232;">g "foo" </span><span style="font-weight:bold;color:#a71d5d;">= </span><span style="color:#0086b3;">MkAnyGADT</span><span style="color:#323232;"> (</span><span style="color:#0086b3;">I</span><span style="color:#323232;"> [</span><span style="color:#0086b3;">42</span><span style="color:#323232;">])
</span><span style="color:#323232;">g </span><span style="color:#183691;">"bar" </span><span style="font-weight:bold;color:#a71d5d;">= </span><span style="color:#0086b3;">MkAnyGADT</span><span style="color:#323232;"> (</span><span style="color:#0086b3;">I</span><span style="color:#323232;"> [</span><span style="color:#0086b3;">69</span><span style="color:#323232;">])
</span><span style="color:#323232;">g x </span><span style="font-weight:bold;color:#a71d5d;">= </span><span style="color:#0086b3;">MkAnyGADT</span><span style="color:#323232;"> (</span><span style="color:#0086b3;">S</span><span style="color:#323232;"> x)
</span><span style="color:#323232;">
</span><span style="font-weight:bold;color:#795da3;">g' </span><span style="font-weight:bold;color:#a71d5d;">:: String -> Scott_Any
</span><span style="color:#323232;">g' "foo" x </span><span style="font-weight:bold;color:#a71d5d;">= </span><span style="color:#323232;">x (</span><span style="font-weight:bold;color:#a71d5d;"></span><span style="color:#323232;">i _s </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> i [</span><span style="color:#0086b3;">42</span><span style="color:#323232;">])
</span><span style="color:#323232;">g' </span><span style="color:#183691;">"bar"</span><span style="color:#323232;"> x </span><span style="font-weight:bold;color:#a71d5d;">=</span><span style="color:#323232;"> x (</span><span style="font-weight:bold;color:#a71d5d;"></span><span style="color:#323232;">i _s </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> i [</span><span style="color:#0086b3;">69</span><span style="color:#323232;">])
</span><span style="color:#323232;">g' s x </span><span style="font-weight:bold;color:#a71d5d;">=</span><span style="color:#323232;"> x (</span><span style="font-weight:bold;color:#a71d5d;"></span><span style="color:#323232;">_i s' </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> s' s)
</span><span style="color:#323232;">
</span><span style="color:#323232;">main </span><span style="font-weight:bold;color:#a71d5d;">=</span><span style="color:#323232;"> interact (unlines </span><span style="font-weight:bold;color:#a71d5d;">.</span><span style="color:#323232;"> fmap x </span><span style="font-weight:bold;color:#a71d5d;">.</span><span style="color:#323232;"> lines)
</span><span style="color:#323232;"> </span><span style="font-weight:bold;color:#a71d5d;">where
</span><span style="color:#323232;">  x s </span><span style="font-weight:bold;color:#a71d5d;">= case</span><span style="color:#323232;"> g s </span><span style="font-weight:bold;color:#a71d5d;">of</span><span style="color:#323232;"> { </span><span style="color:#0086b3;">MkAnyGADT</span><span style="color:#323232;"> x </span><span style="font-weight:bold;color:#a71d5d;">-></span><span style="color:#323232;"> f x }
</span><span style="color:#323232;">  y s </span><span style="font-weight:bold;color:#a71d5d;">=</span><span style="color:#323232;"> g' s f'
</span>

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.