<div dir="ltr"><div><div><div><div><div><div><div><div><div><div><div><div><div><div>> 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?<br><br></div>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.<br></div><div>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.<br></div><div><br>However if your set of types is finite you have other ways of doing what you want:<br><br></div>You can use a GADT to witness this set:<br><br></div>data Witness a where<br></div>  WBool :: Witness Bool<br></div>  WChar :: Witness Char<br><br></div>and then use the witness in your function:<br>transfromTF :: Witness a -> a -> TF a<br><br></div>When you pattern match on say WBool, 'a' will be unified with 'Bool' and the type function will reduce to TypeA<br><br></div>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<br><br></div>data MyType = MyBool | MyChar<br></div>$(singleton ''MyType) -- might me something different haven't used singletons in a while<br><br></div>type family Interpret t where<br></div>  Interpret MyBool = Bool<br></div>  Interpret MyChar = Char<br><br></div><div>and then:<br><br></div><div>transformTF :: Sing t -> Interpret t -> TF t<br></div><div><div><div><div><div><div><div><br></div></div></div></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 31 December 2014 at 16:54, Julian Arni <span dir="ltr"><<a href="mailto:jkarni@gmail.com" target="_blank">jkarni@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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:<br><br>data TypeA = TypeA<br><br><br>type family TF where<br>  TF Bool = TypeA<br><br>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:<br><br>data TypeB = TypeB<br><br>type family TF where<br>  TF Bool = TypeA<br>  TF Char = TypeB<br><br>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.<br><br>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?<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Dec 30, 2014 at 6:47 PM, Atze van der Ploeg <span dir="ltr"><<a href="mailto:atzeus@gmail.com" target="_blank">atzeus@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><p dir="ltr">Hi Julian,</p>
<p dir="ltr">Check out my package ctrex. <a href="https://www.haskell.org/haskellwiki/CTRex" target="_blank">https://www.haskell.org/haskellwiki/CTRex</a></p>
<p dir="ltr">Cheers,</p>
<p dir="ltr">Atze</p>
</span><div class="gmail_quote"><span>On Dec 30, 2014 6:20 PM, "Julian Arni" <<a href="mailto:jkarni@gmail.com" target="_blank">jkarni@gmail.com</a>> wrote:<br type="attribution"></span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><div dir="ltr">Hi all,<br><br>I've been playing around with what might be described as type-directed <br>functions. One example is a list-like structure of phantom-typed values<br><br>{-# LANGUAGE TypeOperators #-}<br>{-# LANGUAGE DataKinds #-}<br>{-# LANGUAGE PolyKinds #-}<br><br>import GHC.TypeLits<br><br>infixr 6 :::<br>data a ::: b = a ::: b<br>             deriving (Show, Eq)<br><br>data Tag b = Tag String<br>           deriving (Show, Eq)<br><br>ex1 :: Tag 5 ::: Tag 3 ::: Tag 7<br>ex1 = Tag "Alice" ::: Tag "Bob" ::: Tag "Carol"<br><br><br>And then sorting 'ex1' based on the Nats, such that <br><br>sort ex1 :: Tag 3 ::: Tag 5 ::: Tag 7<br>sort ex1 = Tag "Bob" ::: Tag "Alice" ::: Tag "Carol"<br><br>Notice how it's the types, not the values, that determine the result, but <br>that the value-level also changes.<br><br>I know how to do this using classes, but it's a little excruciating - it's<br>like programming in a verbose and very restricted Prolog. With type families<br>it's much easier to get the result *type* (pattern matching is simple,<br>recursive calls are natural, and it all looks a lot more like Haskell), but <br>I haven't yet seen a way of effectively using type families to direct <br>the value-level component of the calculation. <br><br>Are there any examples of how this might be done? Or are there other <br>alternatives to using type-classes that I am missing? Or, alternatively, are<br>there libraries to reduce the boilerplate of this type-class code?<br><br>Thanks,<br>  Julian<br><br></div>
<br></div></div><span>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></span></blockquote></div>
</blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>