[Haskell-cafe] Type-directed functions

[Andras Slemmer]

> 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 at 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 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
>>>
>>>
>
> _______________________________________________
> 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/20150102/6f7fc77f/attachment.html>