Hi,
Claus Reinke wrote:
One remaining issue is whether this encoding can be modified to allow
for multiple independent instantiations of 'LA', 'LB', and 'LC' above,
each with their own type parameters, in the same program.
Modules A and B can make their dependence on the ultimate client
Hi again,
Tillmann Rendel wrote:
{-# LANGUAGE TypeFamilies #-}
module D (ok) where
import A
import B
data D client = D client
type family Label client
type instance A.Label (D client) = D.Label client
type instance B.Label (D client) = D.Label client
ok ::
z :: client - Label client
z client = undefined
ok :: (B.Label client ~ A.Label client) =
client - [A.Label client].
ok client = [ A.z client, B.z client]
This technique relies on the explicit management of the identities of
modules both at compile-time (type annotation
Standard ML's answer to that kind of issue is type sharing.
Does type sharing help with making modules retroactively compatible?
It would be as if one could write modules parameterised by types,
instead of declaring them locally, and being able to share a type
parameter over several imports:
Hi Claus,
thanks for your elaborations. I'm still not convinced that a common name
(e.g. TT :. Tr :. Tu :. Te) is a better interface than a common import
(e.g. TypeLevel.Bool.True). In both cases, the authors of all modules
have to actively collaborate, either to define common names, or to
thanks for your elaborations. I'm still not convinced that a common name
(e.g. TT :. Tr :. Tu :. Te) is a better interface than a common import
(e.g. TypeLevel.Bool.True). In both cases, the authors of all modules
have to actively collaborate, either to define common names, or to
define common
in case anyone stumbles over my ad-hoc notations, that should have been:
module A[type label] where x = undefined :: label
module B[type label] where x = undefined :: label
module C[type label] where
import A[label]
import B[label]
ok = [A.x,B.x]
assuming that:
- 'module X[types]' means a
Am Dienstag, 14. April 2009 20:01 schrieb Tillmann Rendel:
How is the need for a common import for 'data TTrue; data TFalse'
different then the need for a common import for 'data Bool = True | False'?
Why not say
data True
data False,
instead of
data TTrue
data TFalse?
I
- if type-level tags (such as 'data TTrue'/'data TFalse') are declared
repeatedly in separate modules, they represent separate types,
preventing shared use (your type-level predicate doesn't return
my version of 'TTrue'/'TFalse')
How is the need for a common import for 'data TTrue;
The recent GHC trac ticket revision reminded me of the old open
type-sharing problem with type tags and record labels:
- if type-level tags (such as 'data TTrue'/'data TFalse') are declared
repeatedly in separate modules, they represent separate types,
preventing shared use (your
- if type-level tags (such as 'data TTrue'/'data TFalse') are declared
repeatedly in separate modules, they represent separate types,
preventing shared use (your type-level predicate doesn't return
my version of 'TTrue'/'TFalse')
How is the need for a common import for 'data TTrue;
11 matches
Mail list logo
