[Haskell-cafe] Type-directed functions

[Julian Arni]

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 at 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 at 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141231/db43d500/attachment.html>