I guess that's my basic question: can one write a function that, for a type family of arbitrary structure (possibly recursive or mutually recusrive, multiple cases) "implements" (i.e., has the corresponding signatures of) that type family?

No, a function like that wouldn't be as parametric as it's type suggests. In other words you would be able to "pattern match" on types, which would result in a broken type system. For example the parametricity of the type (a -> a) implies that the only inhabitant is the identity function (modulo bottom values). With a function like (a -> TF a) where you can "inspect" 'a' you would be able to write a function (a -> a) that is the identity most of the time, *except* for Ints for which it always returns 0. However if your set of types is finite you have other ways of doing what you want: You can use a GADT to witness this set: data Witness a where WBool :: Witness Bool WChar :: Witness Char and then use the witness in your function: transfromTF :: Witness a -> a -> TF a When you pattern match on say WBool, 'a' will be unified with 'Bool' and the type function will reduce to TypeA Another option is to use DataKinds to create an enumeration of your set of types, and use singletons to derive the witness for the lifted type. This is essentially the same as before, only the GADT is derived for you data MyType = MyBool | MyChar $(singleton ''MyType) -- might me something different haven't used singletons in a while type family Interpret t where Interpret MyBool = Bool Interpret MyChar = Char and then: transformTF :: Sing t -> Interpret t -> TF t On 31 December 2014 at 16:54, Julian Arni <jkarni@gmail.com> wrote:

Assuming you mean things like the 'Extend' type family, and 'extend' function, this illustrates one of the doubts I have. In particular, if I have a type family:

data TypeA = TypeA

type family TF where TF Bool = TypeA

then I can write a corresponding function with signature Bool -> TF Bool (since there is only one case for the type family). But suppose I extend TF:

data TypeB = TypeB

type family TF where TF Bool = TypeA TF Char = TypeB

Now, I want to write a function "transformTF :: a -> TF a", but 'a' should really just be restricted to those cases for which 'TF a' is defined. I can obviously do this with fundeps or ATPs (and a class constraint), but then I'm moving in the type-class direction, and, as far as I can tell, no longer benefit from having type families at all. I guess I could also explicitly pass dictionaries, but that seems even worse.

I guess that's my basic question: can one write a function that, for a type family of arbitrary structure (possibly recursive or mutually recusrive, multiple cases) "implements" (i.e., has the corresponding signatures of) that type family?

On Tue, Dec 30, 2014 at 6:47 PM, Atze van der Ploeg <atzeus@gmail.com> wrote:

...

Hi Julian,

Check out my package ctrex. https://www.haskell.org/haskellwiki/CTRex

Cheers,

Atze On Dec 30, 2014 6:20 PM, "Julian Arni" <jkarni@gmail.com> wrote:

...

Hi all,

I've been playing around with what might be described as type-directed functions. One example is a list-like structure of phantom-typed values

{-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-}

import GHC.TypeLits

infixr 6 ::: data a ::: b = a ::: b deriving (Show, Eq)

data Tag b = Tag String deriving (Show, Eq)

ex1 :: Tag 5 ::: Tag 3 ::: Tag 7 ex1 = Tag "Alice" ::: Tag "Bob" ::: Tag "Carol"

And then sorting 'ex1' based on the Nats, such that

sort ex1 :: Tag 3 ::: Tag 5 ::: Tag 7 sort ex1 = Tag "Bob" ::: Tag "Alice" ::: Tag "Carol"

Notice how it's the types, not the values, that determine the result, but that the value-level also changes.

I know how to do this using classes, but it's a little excruciating - it's like programming in a verbose and very restricted Prolog. With type families it's much easier to get the result *type* (pattern matching is simple, recursive calls are natural, and it all looks a lot more like Haskell), but I haven't yet seen a way of effectively using type families to direct the value-level component of the calculation.

Are there any examples of how this might be done? Or are there other alternatives to using type-classes that I am missing? Or, alternatively, are there libraries to reduce the boilerplate of this type-class code?

Thanks, Julian

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

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