Re: [Haskell-cafe] Records and associated types

[Wolfgang Jeltsch]

Am Donnerstag, 11. Dezember 2008 22:04 schrieb Taru Karttunen:
> Hello
>
> What is the correct way to transform code that uses record selection
> with TypeEq (like HList) to associated types?

Hello Taru,

you might want to look at



and its follow-ups.

Best wishes,
Wolfgang
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Records and associated types

[Ryan Ingram]

I don't think you can get a type equality comparison test into type
families without additional compiler support.  If you are willing to
restrict your labels to type-level naturals or some other closed
universe, and allow undecidable instances, you can do something like
this:

data Z   = Z
data S a = S a

type family Select label record
type instance Select lbl (rlbl, ty, rest) = IfEq lbl rlbl ty (Select lbl rest)

type family IfEq n0 n1 t f
type instance IfEq Z Z t f = t
type instance IfEq Z (S n) t f = f
type instance IfEq (S n) Z t f = f
type instance IfEq (S n0) (S n1) t f = IfEq n0 n1 t f

Better support for closed type families that allowed overlap would be
quite useful.

   -- ryan

2008/12/11 Taru Karttunen :
> Hello
>
> What is the correct way to transform code that uses record selection
> with TypeEq (like HList) to associated types? I keep running into
> problems with overlapping type families which is not allowed unless
> they match.
>
> The fundep code:
>
> class Select rec label val | rec label -> val
> instance TypeEq label label True => Select (Label label val :+: rest) label 
> val
> instance (Select tail field val) => Select (any :+: tail) field val
>
> And a conversion attempt:
>
> class SelectT rec label where
>type S rec label
> instance TypeEq label label True => SelectT (Label label val :+: rest) label 
> where
>type S (Label label val :+: rest) label = val
> instance (SelectT tail field) => SelectT (any :+: tail) field where
>type S (any :+: tail) field = S tail field
>
> which fails with:
>
>Conflicting family instance declarations:
>  type instance S (Label label val :+: rest) label
>-- Defined at t.hs:19:9
>  type instance S (any :+: tail) field -- Defined at t.hs:23:9
>
>
> How is it possible to get the TypeEq constraint into the type family?
>
>
> Attached is a complete example that illustrates the problem.
>
>
> - Taru Karttunen
>
> ___
> 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

[Haskell-cafe] Records and associated types

[Taru Karttunen]

Hello

What is the correct way to transform code that uses record selection
with TypeEq (like HList) to associated types? I keep running into
problems with overlapping type families which is not allowed unless
they match.

The fundep code:

class Select rec label val | rec label -> val
instance TypeEq label label True => Select (Label label val :+: rest) label val
instance (Select tail field val) => Select (any :+: tail) field val

And a conversion attempt:

class SelectT rec label where
type S rec label
instance TypeEq label label True => SelectT (Label label val :+: rest) label 
where
type S (Label label val :+: rest) label = val
instance (SelectT tail field) => SelectT (any :+: tail) field where
type S (any :+: tail) field = S tail field

which fails with:

Conflicting family instance declarations:
  type instance S (Label label val :+: rest) label
-- Defined at t.hs:19:9
  type instance S (any :+: tail) field -- Defined at t.hs:23:9


How is it possible to get the TypeEq constraint into the type family?


Attached is a complete example that illustrates the problem.


- Taru Karttunen
{-# LANGUAGE 
  UndecidableInstances, OverlappingInstances, FunctionalDependencies, 
  TypeFamilies, TypeOperators, EmptyDataDecls, GADTs, MultiParamTypeClasses,
  FlexibleInstances
  #-}

-- Fundeps - this works

class Select rec label val | rec label -> val
instance TypeEq label label True => Select (Label label val :+: rest) label val
instance (Select tail field val) => Select (any :+: tail) field val


-- Associated types

class SelectT rec label where
type S rec label
instance TypeEq label label True => SelectT (Label label val :+: rest) label where
type S (Label label val :+: rest) label = val

-- THIS FAILS (comment to get this to compile):
instance (SelectT tail field) => SelectT (any :+: tail) field where
type S (any :+: tail) field = S tail field

{-
ERROR:
Conflicting family instance declarations:
  type instance S (Label label val :+: rest) label
-- Defined at t.hs:19:9
  type instance S (any :+: tail) field -- Defined at t.hs:23:9
-}


-- Support code, to get it compile

data True
data False

type family TypeEqR a b
type instance TypeEqR a a = True

class TypeEq a b result
instance (TypeEqR a b ~ isEq, Proxy2 isEq result) => TypeEq a b result

class Proxy2 inp out
instance (result ~ True) => Proxy2 True result
instance (result ~ False) => Proxy2 notTrue result

data End
data (:+:) a b

infixr :+:

newtype Rec wrap rtype = Rec (OuterWrap wrap (R wrap rtype))

type family InnerWrap wrap t :: *
type family OuterWrap wrap t :: *

data R wrap rtype where
End   :: R wrap End
(:+:) :: InnerWrap wrap x -> R wrap xs -> R wrap (x :+: xs)

data Label l t
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe