[Haskell-cafe] Higher order type functions

[Matt]

Fantastic, thanks so much!

Matt Parsons

On Sat, May 28, 2016 at 10:00 AM, Alexander Vieth <aovieth at gmail.com> wrote:

> Ollie has sent you down the right path. I just want to add these relevant
> links
>
>
> https://www.reddit.com/r/haskell/comments/4354x7/promoting_the_arrow_type/?ref=share&ref_source=link
> https://github.com/avieth/type-function
>
> Alex
>
> On Sat, May 28, 2016 at 7:23 AM, Oliver Charles <ollie at ocharles.org.uk>
> wrote:
>
>> I believe that in order to pass around this partially-applied GreaterThan
>> symbol you're going to need to use defunctionalisation. Richard Eisenberg
>> has a blog post on this ("defunctionalisation for the win") which should
>> get you on the right track.
>>
>> Hope this helps, and happy to be corrected by others of I'm sending you
>> down the wrong path!
>>
>> Ollie
>>
>> On Sat, 28 May 2016, 1:22 a.m. Matt, <parsonsmatt at gmail.com> wrote:
>>
>>> Hi folks!
>>>
>>> I'm playing with GHC 8 and have the following type family definend:
>>>
>>> type family InsertSorted (gt :: k -> k -> Bool) (a :: k) (xs :: [k]) ::
>>> [k] where
>>>     InsertSorted f a '[] = '[a]
>>>     InsertSorted f a (x ': xs) = If (f a x) (x ': InsertSorted f a xs)
>>> (a ': x ': xs)
>>>
>>> With appropriate type functions, I can evaluate this in GHCi with
>>> `:kind!` and it does what I want:
>>>
>>> λ> :kind! InsertSorted GreaterThan One '[Two, Four]
>>> InsertSorted GreaterThan One '[Two, Four] :: [Face]
>>> = '['One, 'Two, 'Four]
>>> λ> :kind! InsertSorted GreaterThan Queen '[Two, Four]
>>> InsertSorted GreaterThan Queen '[Two, Four] :: [Face]
>>> = '['Two, 'Four, 'Queen]
>>>
>>> However, I get an error if I try to use this in a type signature. This
>>> code:
>>>
>>> data Deck (b :: [k]) where
>>>     Empty :: Deck '[]
>>>     (:::) :: CardT s f
>>>           -> Deck xs
>>>           -> Deck (InsertSorted GreaterThan '(s, f) xs)
>>>
>>> gives me this error:
>>>
>>>     • The type family ‘GreaterThan’ should have 2 arguments, but has
>>> been given
>>> none
>>>     • In the definition of data constructor ‘:::’
>>>       In the data type declaration for ‘Deck’
>>>
>>>
>>> What's the best way to use higher order type families?
>>>
>>> Thanks!
>>> Matt Parsons
>>>
>>> Here's the definitions I'm using for the above code:
>>>
>>> data Face
>>>     = One | Two | Three | Four | Five | Six | Seven | Eight | Nine
>>>     | Jack | Queen | King
>>>     deriving (Eq, Ord, Bounded, Enum)
>>>
>>> type family FaceOrd (a :: Face) (b :: Face) :: Ordering where
>>>     FaceOrd a a = 'EQ
>>>     FaceOrd a 'One = 'GT
>>>     FaceOrd 'One a = 'LT
>>>     FaceOrd a b = FaceOrd (PredFace a) (PredFace b)
>>>
>>> type family FaceGT (a :: Face) (b :: Face) :: Bool where
>>>     FaceGT a b = CompK a b == GT
>>>
>>> class GtK (a :: k) where
>>>     type GreaterThan (a :: k) (b :: k) :: Bool
>>>
>>> instance GtK (a :: Face) where
>>>     type GreaterThan a b = CompK a b == GT
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160528/fc7ef224/attachment.html>