Agda refers to things not in scope [Re: [Agda] [ANNOUNCE] Agda 2.5.1]

[Andreas Abel]

Andy, Haskell is no better:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

module BitVector where

data Nat = Z | S Nat

data Vec :: Nat -> * where
   Vnil  :: Vec Z
   Vcons :: Bool -> Vec n -> Vec (S n)


module Main where

import BitVector (Vec(..))

test = Vcons True Vnil


*Main> :load "/home/abel/play/haskell/gadt/UseBitVector.hs"
[1 of 2] Compiling BitVector        ( BitVector.hs, interpreted )
[2 of 2] Compiling Main             ( 
/home/abel/play/haskell/gadt/UseBitVector.hs, interpreted )
Ok, modules loaded: Main, BitVector.
*Main> :t test
test :: Vec ('BitVector.S 'BitVector.Z)

With dependent types, you need to refer to things which are not in scope 
(unless you force the user to reimport recursively everything that is 
mentioned in any imported type).

Or what would be your suggestion?

Cheers,
Andreas


On 19.04.2016 08:54, Andrew Pitts wrote:
> On 18 April 2016 at 18:07, Bradley Hardy <bch29 at cam.ac.uk> wrote:
>> Hi Andy,
>>
>> I believe it’s the actual definitions of the primitive types and functions that are loaded automatically. The names are a separate matter. The automatic inference of types whose names aren’t in scope happens elsewhere too. If we have modules and definitions like so:
>> …
>
> Thanks for that explanation. I can’t say I find this aspect of Agda’s
> behaviour desirable.
>
> Andy
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/