> 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