Re: [Haskell-cafe] Higher order type functions

Fantastic, thanks so much! Matt Parsons On Sat, May 28, 2016 at 10:00 AM, Alexander Vieth 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 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, 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe